changeset 2311 | 69c51db9481f |
parent 2297 | efcabc6df91a |
child 2335 | e965156e84e3 |
--- a/lib/Tools/installfonts Wed Dec 04 13:10:11 1996 +0100 +++ b/lib/Tools/installfonts Wed Dec 04 13:10:52 1996 +0100 @@ -1,7 +1,9 @@ #!/bin/bash # +# $Id$ +# # DESCRIPTION: install Isabelle symbol fonts -# + PRG=$(basename $0) @@ -22,7 +24,7 @@ [ $# -ne 0 ] && usage -RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) +RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || exit 1 case "$RESULT" in xlsfonts:*)