# HG changeset patch
# User wenzelm
# Date 1667647673 -3600
# Node ID 739edaad4f421b600b8e9de7d74d92a248604e8d
# Parent  7b2dbd093ca2dff54d2869f0632b06c103aee35d
tuned signature;

diff -r 7b2dbd093ca2 -r 739edaad4f42 src/Tools/Graphview/graph_file.scala
--- a/src/Tools/Graphview/graph_file.scala	Sat Nov 05 12:12:33 2022 +0100
+++ b/src/Tools/Graphview/graph_file.scala	Sat Nov 05 12:27:53 2022 +0100
@@ -33,11 +33,12 @@
   }
 
   def write(options: Options, file: JFile, graph: Graph_Display.Graph): Unit = {
-    val the_options = options
+    val graphview_options = options
     val graphview =
-      new Graphview(graph.transitive_reduction_acyclic) { def options = the_options }
+      new Graphview(graph.transitive_reduction_acyclic) {
+        def options: Options = graphview_options
+      }
     graphview.update_layout()
-
     write(file, graphview)
   }