# HG changeset patch # User wenzelm # Date 969400260 -7200 # Node ID 950580516dfacfe0acf0ee3e96b23ce723712b6b # Parent b889474af53fcb30c4d5f2f2c00dd13039e3b4c4 tuned msg; diff -r b889474af53f -r 950580516dfa lib/Tools/install --- a/lib/Tools/install Tue Sep 19 23:50:43 2000 +0200 +++ b/lib/Tools/install Tue Sep 19 23:51:00 2000 +0200 @@ -125,5 +125,5 @@ echo "Terminal=0" >> "$KDEAPP" echo "Name=Isabelle" >> "$KDEAPP" - echo "Please refresh your KDE now!" + echo "Please refresh your KDE desktop now!" fi