changeset 9977 | 32955afeb835 |
parent 9789 | 7e5e6c47c0b5 |
child 9997 | 38598a19e701 |
--- a/lib/scripts/run-smlnj-0.93 Fri Sep 15 16:31:00 2000 +0200 +++ b/lib/scripts/run-smlnj-0.93 Fri Sep 15 16:31:36 2000 +0200 @@ -5,9 +5,8 @@ # License: GPL (GNU GENERAL PUBLIC LICENSE) # # SML/NJ startup script (for 0.93). -# -# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, -# and from settings + +export -n INFILE OUTFILE COMPRESS MLTEXT TERMINATE NOWRITE ISABELLE_TMP ## diagnostics