--- 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"