diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2001-12-12 17:02:04 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2001-12-12 17:02:04 +0000 |
| commit | 1de82829cce602467cf3e39f8704b4f0a199ae83 (patch) | |
| tree | 872c7d6d5adc2205d6246e69c4831b423872c24b /isar/interface | |
| parent | afbe4825bd3eb1a9e76405c59284bd1514385f3a (diff) | |
incorporate smart X11 font installation (used to be in isatool installfonts);
Diffstat (limited to 'isar/interface')
| -rw-r--r-- | isar/interface | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/isar/interface b/isar/interface index 2d129027..715f23bf 100644 --- a/isar/interface +++ b/isar/interface @@ -141,6 +141,27 @@ else fi +## smart X11 font installation + +function checkfonts () +{ + XLSFONTS=$(xlsfonts -fn "-xsymb-xsymb0-*" 2>&1) || return 1 + + case "$XLSFONTS" in + xlsfonts:*) + return 1 + ;; + esac + + return 0 +} + +function installfonts () +{ + checkfonts "$XSYMBOL_PATTERN" || eval $XSYMBOL_INSTALLFONTS +} + + ## main if [ "$START_PG" = false ]; then @@ -156,7 +177,7 @@ else if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then ARGS="$ARGS -T Isabelle" - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && "$ISATOOL" installfonts -x + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && installfonts else ARGS="$ARGS -nw" XSYMBOL=false |