ISABELLE_TMP;
authorwenzelm
Mon Dec 01 18:22:02 1997 +0100 (1997-12-01)
changeset 43331d326b826851
parent 4332 d4a15e32c024
child 4334 e567f3425267
ISABELLE_TMP;
bin/isabelle
lib/scripts/run-polyml
lib/scripts/run-smlnj
lib/scripts/run-smlnj-0.93
     1.1 --- a/bin/isabelle	Mon Dec 01 14:42:30 1997 +0100
     1.2 +++ b/bin/isabelle	Mon Dec 01 18:22:02 1997 +0100
     1.3 @@ -155,12 +155,28 @@
     1.4  esac
     1.5  
     1.6  
     1.7 +## prepare tmp directory
     1.8 +
     1.9 +[ -z "$ISABELLE_TMP_PREFIX" ] && ISABELLE_TMP_PREFIX=/tmp/isabelle
    1.10 +
    1.11 +ISABELLE_TMP="$ISABELLE_TMP_PREFIX$$"
    1.12 +mkdir -p "$ISABELLE_TMP"
    1.13 +
    1.14 +
    1.15  ## run it!
    1.16  
    1.17  ML_SYSTEM_BASE=$(echo $ML_SYSTEM | cut -f1 -d-)
    1.18  
    1.19  [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
    1.20  
    1.21 -export INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    1.22 -[ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ] && exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
    1.23 -exec $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
    1.24 +export INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP
    1.25 +
    1.26 +if [ -f $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM ]; then
    1.27 +  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM
    1.28 +else
    1.29 +  $ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE
    1.30 +fi
    1.31 +
    1.32 +
    1.33 +#Do not even think of 'rm -r'!!
    1.34 +rmdir $ISABELLE_TMP
     2.1 --- a/lib/scripts/run-polyml	Mon Dec 01 14:42:30 1997 +0100
     2.2 +++ b/lib/scripts/run-polyml	Mon Dec 01 18:22:02 1997 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  #
     2.5  # Poly/ML startup script.
     2.6  #
     2.7 -# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
     2.8 +# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     2.9  # and from settings
    2.10  
    2.11  
     3.1 --- a/lib/scripts/run-smlnj	Mon Dec 01 14:42:30 1997 +0100
     3.2 +++ b/lib/scripts/run-smlnj	Mon Dec 01 18:22:02 1997 +0100
     3.3 @@ -4,7 +4,7 @@
     3.4  #
     3.5  # SML/NJ startup script (for 1.09.27 or later).
     3.6  #
     3.7 -# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
     3.8 +# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     3.9  # and from settings
    3.10  
    3.11  
     4.1 --- a/lib/scripts/run-smlnj-0.93	Mon Dec 01 14:42:30 1997 +0100
     4.2 +++ b/lib/scripts/run-smlnj-0.93	Mon Dec 01 18:22:02 1997 +0100
     4.3 @@ -4,7 +4,7 @@
     4.4  #
     4.5  # SML/NJ startup script (for 0.93).
     4.6  #
     4.7 -# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
     4.8 +# Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE ISABELLE_TMP,
     4.9  # and from settings
    4.10  
    4.11