--- a/src/Tools/Graphview/popups.scala Sat Jan 03 20:22:27 2015 +0100
+++ b/src/Tools/Graphview/popups.scala Sat Jan 03 20:28:53 2015 +0100
@@ -81,7 +81,7 @@
new Action(to.toString) {
def apply =
add_mutator(
- Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
+ Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to))))
})
})
}
@@ -103,7 +103,7 @@
new Action(from.toString) {
def apply =
add_mutator(
- Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
+ Mutator.make(visualizer, Mutator.Edge_Endpoints((from, to))))
})
})
}