# 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()
 {