Admin/rsync-isabelle
changeset 8398 f1c80ed70f48
child 8544 edaac961e181
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/rsync-isabelle	Thu Mar 09 17:27:54 2000 +0100
     1.3 @@ -0,0 +1,64 @@
     1.4 +#!/bin/sh
     1.5 +#
     1.6 +# mirror script for isabelle distribution
     1.7 +#
     1.8 +# $Id$
     1.9 +#
    1.10 +
    1.11 +## diagnostics
    1.12 +
    1.13 +PRG=`basename "$0"`
    1.14 +
    1.15 +usage()
    1.16 +{
    1.17 +  echo
    1.18 +  echo "Usage: $PRG [OPTIONS] [DEST]"
    1.19 +  echo
    1.20 +  echo "  Options are:"
    1.21 +  echo "    -n    dry run, don't do anything, just report what would happen"
    1.22 +  echo "    -d    delete files that are not on the server (beware!)"
    1.23 +  echo
    1.24 +  exit 1
    1.25 +}
    1.26 +
    1.27 +fail()
    1.28 +{
    1.29 +  echo "$1" >&2
    1.30 +  exit 2
    1.31 +}
    1.32 +
    1.33 +
    1.34 +## process command line
    1.35 +
    1.36 +# options
    1.37 +
    1.38 +ARGS=""
    1.39 +
    1.40 +while getopts "nd" OPT
    1.41 +do
    1.42 +  case "$OPT" in
    1.43 +    n)
    1.44 +      ARGS="$ARGS -n"
    1.45 +      ;;
    1.46 +    d)
    1.47 +      ARGS="$ARGS --delete"
    1.48 +      ;;
    1.49 +    \?)
    1.50 +      usage
    1.51 +      ;;
    1.52 +  esac
    1.53 +done
    1.54 +
    1.55 +shift `expr $OPTIND - 1`
    1.56 +
    1.57 +
    1.58 +# arguments
    1.59 +
    1.60 +[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
    1.61 +
    1.62 +DEST="$1"; shift;
    1.63 +
    1.64 +
    1.65 +## main
    1.66 +
    1.67 +exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."