# HG changeset patch
# User wenzelm
# Date 1420119620 -3600
# Node ID 7b8c50be8d42389fca235cf2d960f20ef56cccac
# Parent  d0edf67253d313b50b677aa9f911473ace36fc03
tuned;

diff -r d0edf67253d3 -r 7b8c50be8d42 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 14:37:25 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Jan 01 14:40:20 2015 +0100
@@ -177,12 +177,12 @@
       }
 
       def typed(c: Char, m: Key.Modifiers) =
-        (c, m) match {
-          case ('+', _) => rescale(Transform.scale * 5.0/4)
-          case ('-', _) => rescale(Transform.scale * 4.0/5)
-          case ('0', _) => Transform.fit_to_window()
-          case ('1', _) => visualizer.Coordinates.update_layout()
-          case ('2', _) => Transform.fit_to_window()
+        c match {
+          case '+' => rescale(Transform.scale * 5.0/4)
+          case '-' => rescale(Transform.scale * 4.0/5)
+          case '0' => Transform.fit_to_window()
+          case '1' => visualizer.Coordinates.update_layout()
+          case '2' => Transform.fit_to_window()
           case _ =>
         }
     }