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