Admin/rsync-isabelle
changeset 11557 66b62cbeaab3
parent 8546 dc053bc2ea06
child 16273 3d5256d3f3f4
equal deleted inserted replaced
11556:8e0768929662 11557:66b62cbeaab3
    15   echo "Usage: $PRG [OPTIONS] DEST"
    15   echo "Usage: $PRG [OPTIONS] DEST"
    16   echo
    16   echo
    17   echo "  Options are:"
    17   echo "  Options are:"
    18   echo "    -h    print help message"
    18   echo "    -h    print help message"
    19   echo "    -n    dry run, don't do anything, just report what would happen"
    19   echo "    -n    dry run, don't do anything, just report what would happen"
    20   echo "    -d    delete files that are not on the server (beware!)"
    20   echo "    -d    delete files that are not on the server (BEWARE!)"
    21   echo
    21   echo
    22   exit 1
    22   exit 1
    23 }
    23 }
    24 
    24 
    25 fail()
    25 fail()