lib/scripts/run-smlnj-0.93
changeset 4333 1d326b826851
parent 3503 390093b95cb0
child 4513 6de428eac512
--- a/lib/scripts/run-smlnj-0.93	Mon Dec 01 14:42:30 1997 +0100
+++ b/lib/scripts/run-smlnj-0.93	Mon Dec 01 18:22:02 1997 +0100
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 0.93).
 #
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
 # and from settings