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