src/Tools/Graphview/src/visualizer.scala
changeset 50471 a5930c929b1e
parent 50470 cb73e91bb019
child 50472 bad1a1ca61e1
--- a/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 20:52:57 2012 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala	Mon Dec 10 21:28:01 2012 +0100
@@ -150,9 +150,7 @@
 
   object Caption
   {
-    def apply(key: String) =
-      if (Parameters.long_names) key
-      else model.complete.get_node(key).name
+    def apply(key: String) = model.complete.get_node(key).name
   }
 
   val font = new Font(Parameters.font_family, Font.BOLD, Parameters.font_size)