changeset 50446 | 8dc05db0bf69 |
parent 49743 | 31bfe82e9220 |
child 50463 | 1d7e506a3a77 |
--- a/src/Tools/Graphview/src/mutator.scala Sun Dec 09 14:01:09 2012 +0100 +++ b/src/Tools/Graphview/src/mutator.scala Sun Dec 09 14:05:21 2012 +0100 @@ -133,7 +133,7 @@ (g, s, d) => !(s == source && d == dest) ) - case class Edge_Transitive() + case class Edge_Transitive() // FIXME slow! / obsolete?! extends Edge_Filter( "Hide transitive edges",