| changeset 2746 | 2a2d51f2cd95 |
| parent 2578 | cc768a16ef65 |
| child 2784 | a78655c814b0 |
--- a/lib/Tools/installfonts Fri Mar 07 09:49:28 1997 +0100 +++ b/lib/Tools/installfonts Fri Mar 07 09:56:55 1997 +0100 @@ -23,7 +23,7 @@ function checkfonts() { - RESULT=$(xlsfonts -fn "-isabelle-*" 2>&1) || return 1 + RESULT=$(xlsfonts -fn "-isabelle-*-isabelle-0" 2>&1) || return 1 case "$RESULT" in xlsfonts:*)