author | wenzelm |
Sun, 28 Dec 1997 15:46:13 +0100 | |
changeset 4494 | 7e5611945959 |
parent 4493 | 26511042ce07 |
child 4495 | 8648ba842d14 |
--- a/src/Pure/ML-Systems/smlnj-0.93.ML Sun Dec 28 15:24:11 1997 +0100 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Sun Dec 28 15:46:13 1997 +0100 @@ -90,7 +90,7 @@ but that function seems to be buggy in SML/NJ 0.93*) fun execute command = let - val tmp_name = getenv "$ISABELLE_TMP" ^ "/isabelle-execute"; + val tmp_name = "/tmp/isabelle-execute"; val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name); val result = input (is, 999999); in