lib/Tools/installfonts
changeset 9788 df671fa2562a
parent 3253 ea75747190a7
child 9974 5361a27c1853
     1.1 --- a/lib/Tools/installfonts	Fri Sep 01 17:48:31 2000 +0200
     1.2 +++ b/lib/Tools/installfonts	Fri Sep 01 17:50:36 2000 +0200
     1.3 @@ -1,11 +1,13 @@
     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: install the isabelle fonts into your X11 server
    1.11  
    1.12  
    1.13 -PRG=$(basename $0)
    1.14 +PRG=$(basename "$0")
    1.15  
    1.16  function usage()
    1.17  {
    1.18 @@ -37,7 +39,7 @@
    1.19  
    1.20  ## main
    1.21  
    1.22 -[ $# -ne 0 ] && usage
    1.23 +[ "$#" -ne 0 ] && usage
    1.24  
    1.25  checkfonts || eval $ISABELLE_INSTALLFONTS
    1.26  checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2