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