author | wenzelm |
Tue, 02 Dec 1997 12:38:39 +0100 | |
changeset 4340 | f5d7fbb73103 |
parent 4339 | b75312b2676d |
child 4341 | 4adf0b093275 |
--- a/src/Pure/ML-Systems/smlnj-0.93.ML Tue Dec 02 12:38:08 1997 +0100 +++ b/src/Pure/ML-Systems/smlnj-0.93.ML Tue Dec 02 12:38:39 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 = "/tmp/.isabelle-execute"; (*let's hope we win the race!*) + val tmp_name = getenv "$ISABELLE_TMP" ^ "/isabelle-execute"; val is = (System.system (command ^ " > " ^ tmp_name); open_in tmp_name); val result = input (is, 999999); in