1 #!/bin/bash
2 # add Isabelle 8bit fonts to X11 font path
3
4 FONTDIR=$ISABELLE8BIT/fonts
5
6 # remove it first to avoid accidental double inclusion
7 xset fp- $FONTDIR 2>/dev/null
8 xset fp+ $FONTDIR