lib/Tools/installfonts
changeset 9788 df671fa2562a
parent 3253 ea75747190a7
child 9974 5361a27c1853
--- a/lib/Tools/installfonts	Fri Sep 01 17:48:31 2000 +0200
+++ b/lib/Tools/installfonts	Fri Sep 01 17:50:36 2000 +0200
@@ -1,11 +1,13 @@
 #!/bin/bash
 #
 # $Id$
+# Author: Markus Wenzel, TU Muenchen
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
 #
 # DESCRIPTION: install the isabelle fonts into your X11 server
 
 
-PRG=$(basename $0)
+PRG=$(basename "$0")
 
 function usage()
 {
@@ -37,7 +39,7 @@
 
 ## main
 
-[ $# -ne 0 ] && usage
+[ "$#" -ne 0 ] && usage
 
 checkfonts || eval $ISABELLE_INSTALLFONTS
 checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2