# HG changeset patch
# User wenzelm
# Date 883320373 -3600
# Node ID 7e5611945959ca47b38f298febaef5e12bea151e
# Parent  26511042ce07b378d2a27fb2b168d089ff13db48
fixed execute;

diff -r 26511042ce07 -r 7e5611945959 src/Pure/ML-Systems/smlnj-0.93.ML
--- 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