author | wenzelm |
Mon, 02 Dec 1996 18:21:50 +0100 | |
changeset 2297 | efcabc6df91a |
child 2311 | 69c51db9481f |
permissions | -rwxr-xr-x |
#!/bin/bash # # 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) case "$RESULT" in xlsfonts:*) xset fp+ $ISABELLE_HOME/lib/fonts xset fp rehash ;; esac