Admin/isasync
changeset 25463 8b9c4582795a
parent 18214 857444b28267
child 36859 51af1657263b
equal deleted inserted replaced
25462:dad0291cb76a 25463:8b9c4582795a
    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 "    -w    mirror whole Isabelle website"
    20   echo "    -w    (ignored for backward compatibility)"
    21   echo "    -d    delete files that are not on the server (BEWARE!)"
    21   echo "    -d    delete files that are not on the server (BEWARE!)"
    22   echo
    22   echo
    23   exit 1
    23   exit 1
    24 }
    24 }
    25 
    25 
    34 
    34 
    35 # options
    35 # options
    36 
    36 
    37 HELP=""
    37 HELP=""
    38 ARGS=""
    38 ARGS=""
    39 SRC="isabelle-distribution"
    39 SRC="isabelle-website"
    40 
    40 
    41 while getopts "hnwd" OPT
    41 while getopts "hnwd" OPT
    42 do
    42 do
    43   case "$OPT" in
    43   case "$OPT" in
    44     h)
    44     h)
    46       ;;
    46       ;;
    47     n)
    47     n)
    48       ARGS="$ARGS -n"
    48       ARGS="$ARGS -n"
    49       ;;
    49       ;;
    50     w)
    50     w)
    51       SRC="isabelle-website"
    51       echo "option -w ignored"
    52       ;;
    52       ;;
    53     d)
    53     d)
    54       ARGS="$ARGS --delete"
    54       ARGS="$ARGS --delete"
    55       ;;
    55       ;;
    56     \?)
    56     \?)