# HG changeset patch # User wenzelm # Date 857725015 -3600 # Node ID 2a2d51f2cd955b537361e5b28e04d9995a60bd6a # Parent 6d0dd9491da89e7a2f9c65ed64b6c42dc0e3c157 more robust check; diff -r 6d0dd9491da8 -r 2a2d51f2cd95 lib/Tools/installfonts --- 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:*)