Admin/rsync-isabelle

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/."