src/Tools/Graphview/etc/options
changeset 59384 c75327a34960
parent 59313 d7f4f46e9a59
child 59393 9f518fa77c1c
equal deleted inserted replaced
59383:1434ef1e0ede 59384:c75327a34960
    18   -- "number of iterations for pendulum method"
    18   -- "number of iterations for pendulum method"
    19 
    19 
    20 public option graphview_iterations_rubberband : int = 10
    20 public option graphview_iterations_rubberband : int = 10
    21   -- "number of iterations for rubberband method"
    21   -- "number of iterations for rubberband method"
    22 
    22 
       
    23 public option graphview_content_margin : int = 60
       
    24   -- "margin for node content pretty-printing"
       
    25