made rsync "official"
authorkleing
Thu Mar 09 17:19:49 2000 +0100 (2000-03-09)
changeset 839616f6de8c897b
parent 8395 919307bebbef
child 8397 f2d371bde3c4
made rsync "official"
Admin/mirror-dist
Admin/mirror-isabelle-dist
     1.1 --- a/Admin/mirror-dist	Thu Mar 09 16:14:37 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Thu Mar 09 17:19:49 2000 +0100
     1.3 @@ -20,4 +20,4 @@
     1.4      ;;
     1.5  esac
     1.6  
     1.7 -rsync -va --delete rsync://www4.in.tum.de:8730/isabelle-dist/. $DEST/.
     1.8 +mirror-isabelle-dist -d $DEST
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/mirror-isabelle-dist	Thu Mar 09 17:19:49 2000 +0100
     2.3 @@ -0,0 +1,76 @@
     2.4 +#!/bin/sh
     2.5 +#
     2.6 +# mirror script for isabelle distribution
     2.7 +#
     2.8 +# $Id$
     2.9 +#
    2.10 +
    2.11 +
    2.12 +
    2.13 +## self references
    2.14 +
    2.15 +PRG=`basename "$0"`
    2.16 +
    2.17 +if [ -h "$0" ]; then
    2.18 +  THIS=`cd \`dirname "$0"\`; cd \`dirname \\\`find "$0" -ls | cut -d ">" -f 2\\\`\`; pwd`
    2.19 +else
    2.20 +  THIS=`cd \`dirname "$0"\`; pwd`
    2.21 +fi
    2.22 +
    2.23 +SUPER=`cd "$THIS/.."; pwd`
    2.24 +
    2.25 +
    2.26 +## diagnostics
    2.27 +
    2.28 +usage()
    2.29 +{
    2.30 +  echo
    2.31 +  echo "Usage: $PRG [OPTIONS] [DEST]"
    2.32 +  echo
    2.33 +  echo "  Options are:"
    2.34 +  echo "    -n    dry run, don't do anything, just report what would happen"
    2.35 +  echo "    -d    delete files that are not on the server"
    2.36 +  echo
    2.37 +  exit 1
    2.38 +}
    2.39 +
    2.40 +fail()
    2.41 +{
    2.42 +  echo "$1" >&2
    2.43 +  exit 2
    2.44 +}
    2.45 +
    2.46 +
    2.47 +## process command line
    2.48 +
    2.49 +# options
    2.50 +
    2.51 +ARGS=""
    2.52 +
    2.53 +while getopts "nd" OPT
    2.54 +do
    2.55 +  case "$OPT" in
    2.56 +    n)
    2.57 +      ARGS="$ARGS -n"
    2.58 +      ;;
    2.59 +    d)
    2.60 +      ARGS="$ARGS --delete"
    2.61 +      ;;
    2.62 +    \?)
    2.63 +      usage
    2.64 +      ;;
    2.65 +  esac
    2.66 +done
    2.67 +
    2.68 +shift `expr $OPTIND - 1`
    2.69 +
    2.70 +
    2.71 +# arguments
    2.72 +
    2.73 +[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
    2.74 +
    2.75 +DEST="$1"; shift;
    2.76 +
    2.77 +## main
    2.78 +
    2.79 +rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. $DEST/.
    2.80 \ No newline at end of file