src/Pure/ML-Systems/smlnj-0.93.ML

 (*execute Unix command which doesn't take any input from stdin and
   sends its output to stdout; could be done more easily by IO.execute,
   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
     close_in is;
     System.Unsafe.SysIO.unlink tmp_name;