# HG changeset patch
# User wenzelm
# Date 881062719 -3600
# Node ID f5d7fbb731038de1e8398ebcdf40329ce78f034a
# Parent  b75312b2676d5335e058dfe67278deadf3285f96
ISABELLE_TMP;

diff -r b75312b2676d -r f5d7fbb73103 src/Pure/ML-Systems/smlnj-0.93.ML
--- 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