Poplog/PML: ML_SUFFIX=.psv;
authorwenzelm
Sat Oct 08 20:15:32 2005 +0200 (2005-10-08)
changeset 17793017e57b1f4d0
parent 17792 4a34fd6884b1
child 17794 87fe1dd02d34
Poplog/PML: ML_SUFFIX=.psv;
etc/settings
     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  ###