etc/options
changeset 50119 5c370a036de7
parent 49524 68796a77c42b
child 50121 97d2b77313a0
equal deleted inserted replaced
50118:89a14e495526 50119:5c370a036de7
    95 option editor_update_delay : real = 0.5
    95 option editor_update_delay : real = 0.5
    96   -- "delay for physical GUI updates"
    96   -- "delay for physical GUI updates"
    97 
    97 
    98 option editor_reparse_limit : int = 10000
    98 option editor_reparse_limit : int = 10000
    99   -- "maximum amount of reparsed text outside perspective"
    99   -- "maximum amount of reparsed text outside perspective"
       
   100 
       
   101 option editor_tracing_limit : int = 1000000
       
   102   -- "maximum tracing volume for each command transaction"