Admin/rsync-isabelle
changeset 11557 66b62cbeaab3
parent 8546 dc053bc2ea06
child 16273 3d5256d3f3f4
     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  }