| changeset 59384 | c75327a34960 |
| parent 59313 | d7f4f46e9a59 |
| child 59393 | 9f518fa77c1c |
--- a/src/Tools/Graphview/etc/options Sat Jan 17 16:40:10 2015 +0100 +++ b/src/Tools/Graphview/etc/options Sat Jan 17 22:20:57 2015 +0100 @@ -20,3 +20,6 @@ public option graphview_iterations_rubberband : int = 10 -- "number of iterations for rubberband method" +public option graphview_content_margin : int = 60 + -- "margin for node content pretty-printing" +