| changeset 2746 | 2a2d51f2cd95 |
| parent 2578 | cc768a16ef65 |
| child 2784 | a78655c814b0 |
| 2745:6d0dd9491da8 | 2746:2a2d51f2cd95 |
|---|---|
21 |
21 |
22 ## check for isabelle fonts |
22 ## check for isabelle fonts |
23 |
23 |
24 function checkfonts() |
24 function checkfonts() |
25 { |
25 { |
26 RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || return 1 |
26 RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1 |
27 |
27 |
28 case "$RESULT" in |
28 case "$RESULT" in |
29 xlsfonts:*) |
29 xlsfonts:*) |
30 return 1 |
30 return 1 |
31 ;; |
31 ;; |