author | wenzelm |
Wed, 04 Dec 1996 13:10:52 +0100 | |
changeset 2311 | 69c51db9481f |
parent 2297 | efcabc6df91a |
child 2335 | e965156e84e3 |
permissions | -rwxr-xr-x |
#!/bin/bash # # $Id$ # # DESCRIPTION: install Isabelle symbol fonts PRG=$(basename $0) function usage() { echo echo "Usage: $PRG" echo echo " Install the Isabelle symbol fonts into your X11 server." echo " (May be savely called repeatedly.)" echo exit 1 } ## main [ $# -ne 0 ] && usage RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || exit 1 case "$RESULT" in xlsfonts:*) xset fp+ $ISABELLE_HOME/lib/fonts xset fp rehash ;; esac