author | wenzelm |
Wed, 04 Dec 1996 13:10:52 +0100 | |
changeset 2311 | 69c51db9481f |
parent 2310 | f49958ca2f8d |
child 2312 | 65ea8bbb4e02 |
--- 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:*)