lib/Tools/installfonts
changeset 2311 69c51db9481f
parent 2297 efcabc6df91a
child 2335 e965156e84e3
     1.1 --- a/lib/Tools/installfonts	Wed Dec 04 13:10:11 1996 +0100
     1.2 +++ b/lib/Tools/installfonts	Wed Dec 04 13:10:52 1996 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4  #!/bin/bash
     1.5  #
     1.6 +# $Id$
     1.7 +#
     1.8  # DESCRIPTION: install Isabelle symbol fonts
     1.9 -#
    1.10 +
    1.11  
    1.12  PRG=$(basename $0)
    1.13  
    1.14 @@ -22,7 +24,7 @@
    1.15  [ $# -ne 0 ] && usage
    1.16  
    1.17  
    1.18 -RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1)
    1.19 +RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || exit 1
    1.20  
    1.21  case "$RESULT" in
    1.22    xlsfonts:*)