lib/Tools/makeall
changeset 9788 df671fa2562a
parent 7277 bb9502f9154a
child 10511 efb3428c9879
     1.1 --- a/lib/Tools/makeall	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/makeall	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,6 +1,8 @@
     1.4  #!/bin/bash
     1.5  #
     1.6  # $Id$
     1.7 +# Author: Markus Wenzel, TU Muenchen
     1.8 +# License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  #
    1.10  # DESCRIPTION: apply make utility to all logics
    1.11  
    1.12 @@ -11,7 +13,7 @@
    1.13  
    1.14  ## diagnostics
    1.15  
    1.16 -PRG=$(basename $0)
    1.17 +PRG=$(basename "$0")
    1.18  
    1.19  function usage()
    1.20  {
    1.21 @@ -36,10 +38,10 @@
    1.22  
    1.23  for L in $ALL_LOGICS
    1.24  do
    1.25 -  ( cd $ISABELLE_HOME/src/$L; $ISATOOL make "$@" )
    1.26 +  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" )
    1.27  done
    1.28  
    1.29  echo -n "Finished at "; date
    1.30  
    1.31 -ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
    1.32 +ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
    1.33  echo "$ELAPSED total elapsed time"