| changeset 2852 | ddb85eb8385f |
| parent 1826 | 2a2c0dbeb4ac |
| 2851:b6a5780e36b9 | 2852:ddb85eb8385f |
|---|---|
1 #!/bin/bash |
1 #!/bin/bash |
2 # add Isabelle 8bit fonts to X11 font path |
|
3 |
2 |
4 FONTDIR=$ISABELLE8BIT/fonts |
3 #NOTE: just a quick and dirty hack -- assumes correct isatool in PATH |
5 |
4 |
6 # remove it first to avoid accidental double inclusion |
5 isatool installfonts |
7 xset fp- $FONTDIR 2>/dev/null |
|
8 xset fp+ $FONTDIR |