| changeset 3253 | ea75747190a7 |
| parent 3007 | e5efa177ee0c |
| child 9788 | df671fa2562a |
| 3252:68c7a70daa16 | 3253:ea75747190a7 |
|---|---|
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG" |
13 echo "Usage: $PRG" |
14 echo |
14 echo |
15 echo " Install the isabelle 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 safely called repeatedly.)" |
17 echo |
17 echo |
18 exit 1 |
18 exit 1 |
19 } |
19 } |
20 |
20 |
21 |
21 |