fails more gracefully;
authorwenzelm
Wed, 04 Dec 1996 13:10:52 +0100
changeset 2311 69c51db9481f
parent 2310 f49958ca2f8d
child 2312 65ea8bbb4e02
fails more gracefully;
lib/Tools/installfonts
--- 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:*)