diff -r df671fa2562a -r 7e5e6c47c0b5 build --- a/build Fri Sep 01 17:50:36 2000 +0200 +++ b/build Fri Sep 01 17:54:58 2000 +0200 @@ -12,11 +12,11 @@ ## settings -PRG=$(basename $0) +PRG=$(basename "$0") export THIS_IS_ISABELLE_BUILD=true -ISABELLE_HOME=$(dirname $0) -. $ISABELLE_HOME/lib/scripts/getsettings || \ +ISABELLE_HOME=$(dirname "$0") +. "$ISABELLE_HOME/lib/scripts/getsettings" || \ { echo "$PRG probably not called from its original place!"; exit 2; } @@ -101,7 +101,7 @@ echo " *****************************" echo echo "Please check $ISABELLE_HOME/etc/settings" - [ -f $ISABELLE_HOME_USER/etc/settings ] && echo "AND $ISABELLE_HOME_USER/etc/settings" + [ -f "$ISABELLE_HOME_USER/etc/settings" ] && echo "AND $ISABELLE_HOME_USER/etc/settings" echo "to make sure that Isabelle's ML system settings and compilation options" echo "are appropriate." echo @@ -130,8 +130,8 @@ for L in $LOGICS do - DIR=$ISABELLE_HOME/src/$L - if [ -f $DIR/IsaMakefile ]; then + DIR="$ISABELLE_HOME/src/$L" + if [ -f "$DIR/IsaMakefile" ]; then MAKE_LOGICS="$MAKE_LOGICS $L" else echo "No such logic: $L" @@ -140,12 +140,12 @@ if [ -z "$BATCH" ]; then - echo " " $MAKE_LOGICS + echo " $MAKE_LOGICS" echo read else echo - echo "Isabelle build:" $MAKE_LOGICS + echo "Isabelle build: $MAKE_LOGICS" echo echo "ML_SYSTEM=$ML_SYSTEM" echo "ML_HOME=$ML_HOME" @@ -166,10 +166,10 @@ for L in $MAKE_LOGICS do - ( cd $ISABELLE_HOME/src/$L; $ISATOOL make $TARGETS ) + ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS ) done echo -n "Finished at "; date -ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS) +ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS") echo "$ELAPSED total elapsed time"