diff -r 8e0768929662 -r 66b62cbeaab3 Admin/rsync-isabelle
--- a/Admin/rsync-isabelle	Sat Sep 08 20:06:13 2001 +0200
+++ b/Admin/rsync-isabelle	Mon Sep 10 13:57:57 2001 +0200
@@ -17,7 +17,7 @@
   echo "  Options are:"
   echo "    -h    print help message"
   echo "    -n    dry run, don't do anything, just report what would happen"
-  echo "    -d    delete files that are not on the server (beware!)"
+  echo "    -d    delete files that are not on the server (BEWARE!)"
   echo
   exit 1
 }