equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
2 # |
2 # |
3 # $Id$ |
3 # $Id$ |
|
4 # Author: Markus Wenzel, TU Muenchen |
|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 # |
6 # |
5 # DESCRIPTION: install the isabelle fonts into your X11 server |
7 # DESCRIPTION: install the isabelle fonts into your X11 server |
6 |
8 |
7 |
9 |
8 PRG=$(basename $0) |
10 PRG=$(basename "$0") |
9 |
11 |
10 function usage() |
12 function usage() |
11 { |
13 { |
12 echo |
14 echo |
13 echo "Usage: $PRG" |
15 echo "Usage: $PRG" |
35 } |
37 } |
36 |
38 |
37 |
39 |
38 ## main |
40 ## main |
39 |
41 |
40 [ $# -ne 0 ] && usage |
42 [ "$#" -ne 0 ] && usage |
41 |
43 |
42 checkfonts || eval $ISABELLE_INSTALLFONTS |
44 checkfonts || eval $ISABELLE_INSTALLFONTS |
43 checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2 |
45 checkfonts || echo "WARNING: Isabelle fonts probably not installed correctly!" >&2 |