# HG changeset patch
# User wenzelm
# Date 880996922 -3600
# Node ID 1d326b82685147f3882b1fb3a2f5332a6e922cfe
# Parent  d4a15e32c0241169e82af870b203e7df4800848e
ISABELLE_TMP;

diff -r d4a15e32c024 -r 1d326b826851 bin/isabelle
--- a/bin/isabelle	Mon Dec 01 14:42:30 1997 +0100
+++ b/bin/isabelle	Mon Dec 01 18:22:02 1997 +0100
@@ -155,12 +155,28 @@
 esac
 
 
+## prepare tmp directory
+
+[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
+
+ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
+mkdir -p "$ISABELLE_TMP"
+
+
 ## run it!
 
 ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
 
 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
 
-export INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
-exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
+export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP
+
+if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
+  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
+else
+  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
+fi
+
+
+#Do not even think of 'rm -r'!!
+rmdir $ISABELLE_TMP
diff -r d4a15e32c024 -r 1d326b826851 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Mon Dec 01 14:42:30 1997 +0100
+++ b/lib/scripts/run-polyml	Mon Dec 01 18:22:02 1997 +0100
@@ -4,7 +4,7 @@
 #
 # Poly/ML startup script.
 #
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
 # and from settings
 
 
diff -r d4a15e32c024 -r 1d326b826851 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Dec 01 14:42:30 1997 +0100
+++ b/lib/scripts/run-smlnj	Mon Dec 01 18:22:02 1997 +0100
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 1.09.27 or later).
 #
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
 # and from settings
 
 
diff -r d4a15e32c024 -r 1d326b826851 lib/scripts/run-smlnj-0.93
--- a/lib/scripts/run-smlnj-0.93	Mon Dec 01 14:42:30 1997 +0100
+++ b/lib/scripts/run-smlnj-0.93	Mon Dec 01 18:22:02 1997 +0100
@@ -4,7 +4,7 @@
 #
 # SML/NJ startup script (for 0.93).
 #
-# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
+# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
 # and from settings