etc/settings
changeset 22148 3b99944136ef
parent 21812 2776dcfd5617
child 23138 6852373aae8a
equal deleted inserted replaced
22147:f4ed4d940d44 22148:3b99944136ef
    60 #ML_HOME="/usr/local/poplog/current-poplog/bin"
    60 #ML_HOME="/usr/local/poplog/current-poplog/bin"
    61 #ML_OPTIONS="-noinit"
    61 #ML_OPTIONS="-noinit"
    62 #ML_SUFFIX=".psv"
    62 #ML_SUFFIX=".psv"
    63 #ML_PLATFORM=""
    63 #ML_PLATFORM=""
    64 
    64 
       
    65 # Alice 1.3 (experimental!)
       
    66 #ML_SYSTEM=alice
       
    67 #ML_HOME="/usr/local/alice/bin"
       
    68 #ML_OPTIONS=""
       
    69 #ML_PLATFORM=""
       
    70 
    65 
    71 
    66 ###
    72 ###
    67 ### Compilation options (cf. isatool usedir)
    73 ### Compilation options (cf. isatool usedir)
    68 ###
    74 ###
    69 
    75