tuned usage;
authorwenzelm
Mon, 10 Sep 2001 13:57:57 +0200
changeset 11557 66b62cbeaab3
parent 11556 8e0768929662
child 11558 6539627881e8
tuned usage;
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
 }