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