equal
deleted
inserted
replaced
728 Parent::notifier(Edge()).erase(arc); |
728 Parent::notifier(Edge()).erase(arc); |
729 std::vector<Arc> dir; |
729 std::vector<Arc> dir; |
730 dir.push_back(arcFromId(n)); |
730 dir.push_back(arcFromId(n)); |
731 dir.push_back(arcFromId(n-1)); |
731 dir.push_back(arcFromId(n-1)); |
732 Parent::notifier(Arc()).erase(dir); |
732 Parent::notifier(Arc()).erase(dir); |
733 nodes[arcs[n].target].first_out=arcs[n].next_out; |
733 nodes[arcs[n-1].target].first_out=arcs[n].next_out; |
734 nodes[arcs[n-1].target].first_out=arcs[n-1].next_out; |
734 nodes[arcs[n].target].first_out=arcs[n-1].next_out; |
735 arcs.pop_back(); |
735 arcs.pop_back(); |
736 arcs.pop_back(); |
736 arcs.pop_back(); |
737 } |
737 } |
738 while(s.node_num<nodes.size()) { |
738 while(s.node_num<nodes.size()) { |
739 int n=nodes.size()-1; |
739 int n=nodes.size()-1; |