diff -r fb8c5a66dbe8 -r df671fa2562a lib/Tools/makeall
--- a/lib/Tools/makeall	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/makeall	Fri Sep 01 17:50:36 2000 +0200
@@ -1,6 +1,8 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: apply make utility to all logics
 
@@ -11,7 +13,7 @@
 
 ## diagnostics
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -36,10 +38,10 @@
 
 for L in $ALL_LOGICS
 do
-  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make "$@" )
+  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" )
 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"