--- a/src/Tools/Graphview/etc/options Tue Jan 06 23:56:13 2015 +0100
+++ b/src/Tools/Graphview/etc/options Wed Jan 07 00:10:23 2015 +0100
@@ -10,3 +10,13 @@
public option graphview_font_scale : real = 0.85
-- "scale factor of graph view wrt. main text font"
+
+public option graphview_iterations_minimize_crossings : int = 40
+ -- "number of iterations to minimize edge crossings"
+
+public option graphview_iterations_pendulum : int = 10
+ -- "number of iterations for pendulum method"
+
+public option graphview_iterations_rubberband : int = 10
+ -- "number of iterations for rubberband method"
+