# HG changeset patch # User wenzelm # Date 974925699 -3600 # Node ID efb3428c98794c1b11638f15a2ec398a89ba90e8 # Parent d243553849ecd3f6c6b5f2983dce9dfbf09b1b16 tuned; diff -r d243553849ec -r efb3428c9879 bin/isabelle --- a/bin/isabelle Wed Nov 22 21:38:26 2000 +0100 +++ b/bin/isabelle Wed Nov 22 21:41:39 2000 +0100 @@ -9,9 +9,9 @@ ## settings -PRG=$(basename "$0") +PRG="$(basename "$0")" -ISABELLE_HOME=$(dirname "$0")/.. +ISABELLE_HOME="$(dirname "$0")/.." . "$ISABELLE_HOME/lib/scripts/getsettings" || \ { echo "$PRG probably not called from its original place!"; exit 2; } diff -r d243553849ec -r efb3428c9879 bin/isatool --- a/bin/isatool Wed Nov 22 21:38:26 2000 +0100 +++ b/bin/isatool Wed Nov 22 21:41:39 2000 +0100 @@ -10,9 +10,9 @@ ## settings -PRG=$(basename "$0") +PRG="$(basename "$0")" -ISABELLE_HOME=$(dirname "$0")/.. +ISABELLE_HOME="$(dirname "$0")/.." . "$ISABELLE_HOME/lib/scripts/getsettings" || \ { echo "$PRG probably not called from its original place!"; exit 2; } diff -r d243553849ec -r efb3428c9879 build --- a/build Wed Nov 22 21:38:26 2000 +0100 +++ b/build Wed Nov 22 21:41:39 2000 +0100 @@ -14,10 +14,10 @@ ## settings -PRG=$(basename "$0") +PRG="$(basename "$0")" export THIS_IS_ISABELLE_BUILD=true -ISABELLE_HOME=$(dirname "$0") +ISABELLE_HOME="$(dirname "$0")" . "$ISABELLE_HOME/lib/scripts/getsettings" || \ { echo "$PRG probably not called from its original place!"; exit 2; } @@ -164,9 +164,7 @@ # build it SECONDS=0 -DATE=$(date) -HOST=$(hostname) -echo "Started at $DATE ($HOST)" +echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" for L in $MAKE_LOGICS do diff -r d243553849ec -r efb3428c9879 configure --- a/configure Wed Nov 22 21:38:26 2000 +0100 +++ b/configure Wed Nov 22 21:41:39 2000 +0100 @@ -8,7 +8,7 @@ ## patch scripts -cd `dirname "$0"` +cd "`dirname "$0"`" if bash -c : then diff -r d243553849ec -r efb3428c9879 lib/Tools/browser --- a/lib/Tools/browser Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/browser Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: Isabelle graph browser -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/doc --- a/lib/Tools/doc Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/doc Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: view Isabelle documentation -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/document --- a/lib/Tools/document Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/document Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: prepare theory session document -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/expandshort --- a/lib/Tools/expandshort Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/expandshort Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: expand shorthand goal commands -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/fixclasimp --- a/lib/Tools/fixclasimp Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/fixclasimp Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/fixdatatype --- a/lib/Tools/fixdatatype Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/fixdatatype Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/fixdots --- a/lib/Tools/fixdots Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/fixdots Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/fixgoal --- a/lib/Tools/fixgoal Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/fixgoal Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/fixseq --- a/lib/Tools/fixseq Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/fixseq Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/fixsome --- a/lib/Tools/fixsome Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/fixsome Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/getenv --- a/lib/Tools/getenv Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/getenv Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/installfonts --- a/lib/Tools/installfonts Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/installfonts Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: install symbol fonts on the current X11 server -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/latex --- a/lib/Tools/latex Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/latex Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: run LaTeX (and related tools) -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/logo --- a/lib/Tools/logo Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/logo Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: create an instance of the Isabelle logo -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/make --- a/lib/Tools/make Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/make Wed Nov 22 21:41:39 2000 +0100 @@ -7,7 +7,7 @@ # DESCRIPTION: Isabelle make utility -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/makeall --- a/lib/Tools/makeall Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/makeall Wed Nov 22 21:41:39 2000 +0100 @@ -13,7 +13,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { @@ -30,11 +30,7 @@ [ "$1" = "-?" ] && usage - -SECONDS=0 -DATE=$(date) -HOST=$(hostname) -echo "Started at $DATE ($HOST)" +echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" for L in $ALL_LOGICS do diff -r d243553849ec -r efb3428c9879 lib/Tools/mkdir --- a/lib/Tools/mkdir Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/mkdir Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/nonascii --- a/lib/Tools/nonascii Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/nonascii Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/unsymbolize --- a/lib/Tools/unsymbolize Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/unsymbolize Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() { diff -r d243553849ec -r efb3428c9879 lib/Tools/usedir --- a/lib/Tools/usedir Wed Nov 22 21:38:26 2000 +0100 +++ b/lib/Tools/usedir Wed Nov 22 21:41:39 2000 +0100 @@ -9,7 +9,7 @@ ## diagnostics -PRG=$(basename "$0") +PRG="$(basename "$0")" function usage() {