Admin/rsync-isabelle
author wenzelm
Thu Mar 09 17:27:54 2000 +0100 (2000-03-09)
changeset 8398 f1c80ed70f48
child 8544 edaac961e181
permissions -rwxr-xr-x
renamed to rsync-isabelle;
     1 #!/bin/sh
     2 #
     3 # mirror script for isabelle distribution
     4 #
     5 # $Id$
     6 #
     7 
     8 ## diagnostics
     9 
    10 PRG=`basename "$0"`
    11 
    12 usage()
    13 {
    14   echo
    15   echo "Usage: $PRG [OPTIONS] [DEST]"
    16   echo
    17   echo "  Options are:"
    18   echo "    -n    dry run, don't do anything, just report what would happen"
    19   echo "    -d    delete files that are not on the server (beware!)"
    20   echo
    21   exit 1
    22 }
    23 
    24 fail()
    25 {
    26   echo "$1" >&2
    27   exit 2
    28 }
    29 
    30 
    31 ## process command line
    32 
    33 # options
    34 
    35 ARGS=""
    36 
    37 while getopts "nd" OPT
    38 do
    39   case "$OPT" in
    40     n)
    41       ARGS="$ARGS -n"
    42       ;;
    43     d)
    44       ARGS="$ARGS --delete"
    45       ;;
    46     \?)
    47       usage
    48       ;;
    49   esac
    50 done
    51 
    52 shift `expr $OPTIND - 1`
    53 
    54 
    55 # arguments
    56 
    57 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
    58 
    59 DEST="$1"; shift;
    60 
    61 
    62 ## main
    63 
    64 exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."