# HG changeset patch
# User wenzelm
# Date 864647139 -7200
# Node ID 943d1630f003f88ad81a569a5a7acbf84b97d99d
# Parent  3f9a806f061eeab57e9f75eb974a88e79625f58a
tuned comment;

diff -r 3f9a806f061e -r 943d1630f003 etc/settings
--- a/etc/settings	Mon May 26 12:54:40 1997 +0200
+++ b/etc/settings	Mon May 26 13:45:39 1997 +0200
@@ -32,7 +32,7 @@
 #ML_HOME=/usr/local/sml107/bin
 #ML_OPTIONS="@SMLdebug=/dev/null"
 
-# Standard ML of New Jersey 1.09.27
+# Standard ML of New Jersey 1.09.27, or later
 #ML_SYSTEM=smlnj-1.09
 #ML_HOME=/usr/local/sml109.27/bin
 #ML_OPTIONS="@SMLdebug=/dev/null"