equal
deleted
inserted
replaced
735 Parent::notifier(Edge()).erase(arc); |
735 Parent::notifier(Edge()).erase(arc); |
736 std::vector<Arc> dir; |
736 std::vector<Arc> dir; |
737 dir.push_back(arcFromId(n)); |
737 dir.push_back(arcFromId(n)); |
738 dir.push_back(arcFromId(n-1)); |
738 dir.push_back(arcFromId(n-1)); |
739 Parent::notifier(Arc()).erase(dir); |
739 Parent::notifier(Arc()).erase(dir); |
740 nodes[arcs[n].target].first_out=arcs[n].next_out; |
740 nodes[arcs[n-1].target].first_out=arcs[n].next_out; |
741 nodes[arcs[n-1].target].first_out=arcs[n-1].next_out; |
741 nodes[arcs[n].target].first_out=arcs[n-1].next_out; |
742 arcs.pop_back(); |
742 arcs.pop_back(); |
743 arcs.pop_back(); |
743 arcs.pop_back(); |
744 } |
744 } |
745 while(s.node_num<nodes.size()) { |
745 while(s.node_num<nodes.size()) { |
746 int n=nodes.size()-1; |
746 int n=nodes.size()-1; |