src/Tools/Graphview/src/mutator.scala
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",