etc/options
changeset 60074 38a64cc17403
parent 59468 fe6651760643
child 60730 02c2860fcf30
     1.1 --- a/etc/options	Wed Apr 15 11:47:29 2015 +0200
     1.2 +++ b/etc/options	Wed Apr 15 13:55:01 2015 +0200
     1.3 @@ -101,6 +101,9 @@
     1.4  public option ML_exception_trace : bool = false
     1.5    -- "ML exception trace for toplevel command execution"
     1.6  
     1.7 +public option ML_statistics : bool = true
     1.8 +  -- "ML runtime system statistics"
     1.9 +
    1.10  
    1.11  section "Editor Reactivity"
    1.12