equal
deleted
inserted
replaced
1 #!/bin/bash -norc |
1 #!/bin/bash -norc |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
4 # |
4 # |
5 # DESCRIPTION: install Isabelle symbol fonts |
5 # DESCRIPTION: install the isabelle fonts into your X11 server |
6 |
6 |
7 |
7 |
8 PRG=$(basename $0) |
8 PRG=$(basename $0) |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG" |
13 echo "Usage: $PRG" |
14 echo |
14 echo |
15 echo " Install the Isabelle symbol fonts into your X11 server." |
15 echo " Install the isabelle fonts into your X11 server." |
16 echo " (May be savely called repeatedly.)" |
16 echo " (May be savely called repeatedly.)" |
17 echo |
17 echo |
18 exit 1 |
18 exit 1 |
19 } |
19 } |
20 |
20 |
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-*-isabelle-0" 2>&1) || return 1 |
26 RESULT=$(xlsfonts -fn "-isabelle-fixed-*-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 ;; |