# HG changeset patch # User wenzelm # Date 864149203 -7200 # Node ID ea75747190a76a2288c0f6bbc8d204dc7fd6d576 # Parent 68c7a70daa1683cdf06df0eec81275138dbd829f fixed spelling; diff -r 68c7a70daa16 -r ea75747190a7 lib/Tools/installfonts --- a/lib/Tools/installfonts Tue May 20 17:58:20 1997 +0200 +++ b/lib/Tools/installfonts Tue May 20 19:26:43 1997 +0200 @@ -13,7 +13,7 @@ echo "Usage: $PRG" echo echo " Install the isabelle fonts into your X11 server." - echo " (May be savely called repeatedly.)" + echo " (May be safely called repeatedly.)" echo exit 1 }