diff -r 76f74ac9edee -r 5e8287d34295 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() }