# HG changeset patch
# User wenzelm
# Date 849701452 -3600
# Node ID 69c51db9481f7e8499ba8a6428a063559f4d2bdb
# Parent  f49958ca2f8dab330e90a589bb7a8ecc8ee6d6c6
fails more gracefully;

diff -r f49958ca2f8d -r 69c51db9481f 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:*)