etc/settings
changeset 27202 1a604efd267d
parent 26908 25fb7241f32e
child 27906 df49b4da8903
     1.1 --- a/etc/settings	Sat Jun 14 17:26:09 2008 +0200
     1.2 +++ b/etc/settings	Sat Jun 14 17:26:10 2008 +0200
     1.3 @@ -67,13 +67,6 @@
     1.4  #ML_OPTIONS=""
     1.5  #ML_PLATFORM=""
     1.6  
     1.7 -# Poplog/PML version 15.6/2.1 (experimental!)
     1.8 -#ML_SYSTEM=poplogml
     1.9 -#ML_HOME="/usr/local/poplog/current-poplog/bin"
    1.10 -#ML_OPTIONS="-noinit"
    1.11 -#ML_SUFFIX=".psv"
    1.12 -#ML_PLATFORM=""
    1.13 -
    1.14  
    1.15  ###
    1.16  ### Interactive sessions (cf. isatool tty)