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