src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Thu Nov 07 11:46:21 2024 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Thu Nov 07 12:08:32 2024 +0100
@@ -298,7 +298,7 @@
     tooltip = "Save current graph layout as PNG or PDF"
   }
 
-  private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(0.01 * factor) }
+  private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(scale) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }