Admin/rsync-isabelle
author wenzelm
Mon, 13 Mar 2000 13:21:39 +0100
changeset 8434 5e4bba59bfaa
parent 8398 f1c80ed70f48
child 8544 edaac961e181
permissions -rwxr-xr-x
use HOLogic.Not; export indexify_names;

#!/bin/sh
#
# mirror script for isabelle distribution
#
# $Id$
#

## diagnostics

PRG=`basename "$0"`

usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [DEST]"
  echo
  echo "  Options are:"
  echo "    -n    dry run, don't do anything, just report what would happen"
  echo "    -d    delete files that are not on the server (beware!)"
  echo
  exit 1
}

fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

ARGS=""

while getopts "nd" OPT
do
  case "$OPT" in
    n)
      ARGS="$ARGS -n"
      ;;
    d)
      ARGS="$ARGS --delete"
      ;;
    \?)
      usage
      ;;
  esac
done

shift `expr $OPTIND - 1`


# arguments

[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }

DEST="$1"; shift;


## main

exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."