| changeset 4333 | 1d326b826851 |
| parent 3503 | 390093b95cb0 |
| child 4505 | 4a2c872b6513 |
--- a/lib/scripts/run-polyml Mon Dec 01 14:42:30 1997 +0100 +++ b/lib/scripts/run-polyml Mon Dec 01 18:22:02 1997 +0100 @@ -4,7 +4,7 @@ # # Poly/ML startup script. # -# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE, +# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP, # and from settings