--- 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
--- 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
--- 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
--- 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