# HG changeset patch
# User wenzelm
# Date 1128795332 -7200
# Node ID 017e57b1f4d01556b04d960a85f05fba07f6f0ac
# Parent  4a34fd6884b12df47317643d277092e5be97a3f4
Poplog/PML: ML_SUFFIX=.psv;

diff -r 4a34fd6884b1 -r 017e57b1f4d0 etc/settings
--- a/etc/settings	Sat Oct 08 20:15:31 2005 +0200
+++ b/etc/settings	Sat Oct 08 20:15:32 2005 +0200
@@ -48,7 +48,7 @@
 #ML_HOME="$ISABELLE_HOME/contrib/poplog/current-poplog/bin"
 #ML_PLATFORM=""
 #ML_OPTIONS="-noinit"
-
+#ML_SUFFIX=".psv"
 
 
 ###