src/Tools/Graphview/graph_panel.scala

--- a/src/Tools/Graphview/graph_panel.scala	Fri Aug 12 11:35:44 2022 +0200
+++ b/src/Tools/Graphview/graph_panel.scala	Fri Aug 12 11:47:12 2022 +0200
@@ -298,7 +298,7 @@
     tooltip = "Save current graph layout as PNG or PDF"
   }
 
-  private val zoom = new GUI.Zoom_Box { def changed() = rescale(0.01 * factor) }
+  private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) }
 
   private val fit_window = new Button {
     action = Action("Fit to window") { fit_to_window() }