tuned usage;
authorwenzelm
Mon Sep 10 13:57:57 2001 +0200 (2001-09-10)
changeset 1155766b62cbeaab3
parent 11556 8e0768929662
child 11558 6539627881e8
tuned usage;
Admin/rsync-isabelle
     1.1 --- a/Admin/rsync-isabelle	Sat Sep 08 20:06:13 2001 +0200
     1.2 +++ b/Admin/rsync-isabelle	Mon Sep 10 13:57:57 2001 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    echo "  Options are:"
     1.5    echo "    -h    print help message"
     1.6    echo "    -n    dry run, don't do anything, just report what would happen"
     1.7 -  echo "    -d    delete files that are not on the server (beware!)"
     1.8 +  echo "    -d    delete files that are not on the server (BEWARE!)"
     1.9    echo
    1.10    exit 1
    1.11  }