etc/options
changeset 49524 68796a77c42b
parent 49295 2750756db9c5
child 50119 5c370a036de7
     1.1 --- a/etc/options	Sat Sep 22 14:03:01 2012 +0200
     1.2 +++ b/etc/options	Sat Sep 22 14:41:41 2012 +0200
     1.3 @@ -95,3 +95,5 @@
     1.4  option editor_update_delay : real = 0.5
     1.5    -- "delay for physical GUI updates"
     1.6  
     1.7 +option editor_reparse_limit : int = 10000
     1.8 +  -- "maximum amount of reparsed text outside perspective"