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)