# HG changeset patch
# User wenzelm
# Date 1142951933 -3600
# Node ID bb3cbf03a021badce756d0bbf0f3c4870069548e
# Parent  e3d48fa3908e69ebe32a491230ea974f421792c4
fixed example;

diff -r e3d48fa3908e -r bb3cbf03a021 etc/settings
--- a/etc/settings	Tue Mar 21 12:18:22 2006 +0100
+++ b/etc/settings	Tue Mar 21 15:38:53 2006 +0100
@@ -32,7 +32,7 @@
 
 # Poly/ML 4.2.0 (manual settings)
 #ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux"
+#ML_HOME=/usr/local/polyml/x86-linux
 #ML_SYSTEM=polyml-4.2.0
 #ML_OPTIONS="-H 80"