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