etc/settings
changeset 17793 017e57b1f4d0
parent 17768 72575258a561
child 17825 ede984daba01
     1.1 --- a/etc/settings	Sat Oct 08 20:15:31 2005 +0200
     1.2 +++ b/etc/settings	Sat Oct 08 20:15:32 2005 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  #ML_HOME="$ISABELLE_HOME/contrib/poplog/current-poplog/bin"
     1.5  #ML_PLATFORM=""
     1.6  #ML_OPTIONS="-noinit"
     1.7 -
     1.8 +#ML_SUFFIX=".psv"
     1.9  
    1.10  
    1.11  ###