etc/options
changeset 63986 c7a4b03727ae
parent 63827 b24d0e53dd03
child 64130 e17c211a0bb6
     1.1 --- a/etc/options	Sat Oct 01 20:59:09 2016 +0200
     1.2 +++ b/etc/options	Sat Oct 01 23:05:25 2016 +0200
     1.3 @@ -129,6 +129,9 @@
     1.4  public option ML_system_64 : bool = false
     1.5    -- "ML system for 64bit platform is used if possible (change requires restart)"
     1.6  
     1.7 +public option ML_process_policy : string = ""
     1.8 +  -- "ML process command prefix (process policy)"
     1.9 +
    1.10  
    1.11  section "Editor Reactivity"
    1.12