author | wenzelm |
Mon, 09 Dec 1996 09:04:07 +0100 | |
changeset 2335 | e965156e84e3 |
parent 2311 | 69c51db9481f |
child 2578 | cc768a16ef65 |
permissions | -rwxr-xr-x |
#!/bin/bash -norc # # $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