etc/options
changeset 60843 9980f3bcdea2
parent 60765 e43e71a75838
child 60845 c4cb46e3cdd1
     1.1 --- a/etc/options	Wed Aug 05 14:18:07 2015 +0200
     1.2 +++ b/etc/options	Wed Aug 05 16:13:42 2015 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4    -- "ML debugger in single-step mode"
     1.5  
     1.6  public option ML_statistics : bool = true
     1.7 -  -- "ML runtime system statistics"
     1.8 +  -- "ML run-time system statistics"
     1.9  
    1.10  
    1.11  section "Editor Reactivity"