# HG changeset patch # User Paul Boddie # Date 1527613375 -7200 # Node ID 37b1f1aefe070c1372fe0a54fdeb073fd3fdf12f # Parent b921e4f8cd4c8602b291a3bc5210ca140a6db5d0 Report font generation problems and exit if they occur. diff -r b921e4f8cd4c -r 37b1f1aefe07 tools/install.sh --- a/tools/install.sh Tue May 29 19:01:38 2018 +0200 +++ b/tools/install.sh Tue May 29 19:02:55 2018 +0200 @@ -56,7 +56,13 @@ # Generate binaries if appropriate. if [ ! "$CLEAN" ] ; then - "$THISDIR/makefonts.sh" -q + if ! "$THISDIR/makefonts.sh" -q ; then + cat 1>&2 <&2 <. """ -from os.path import split +from os.path import isfile, split import sys def convert_font(fin, fout, points, missing=32): @@ -233,6 +233,10 @@ # Convert from the input to the output file. else: + if not isfile(filename_or_option): + print >>sys.stderr, "Font file not found:", filename_or_option + sys.exit(1) + fin = open(filename_or_option) fout = open(tff_filename, "w") try: