--- 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)
}