diff -r cd0a411b7fc1 -r 76b6207eb000 Admin/isasync
--- a/Admin/isasync	Thu Jul 05 13:35:46 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,129 +0,0 @@
-#!/usr/bin/env bash
-#
-# mirror script for Isabelle distribution or website
-
-
-## diagnostics
-
-PRG=`basename "$0"`
-
-usage()
-{
-  echo
-  echo "Usage: $PRG [OPTIONS] DEST"
-  echo
-  echo "  Options are:"
-  echo "    -h    print help message"
-  echo "    -n    dry run, don't do anything, just report what would happen"
-  echo "    -w    (ignored for backward compatibility)"
-  echo "    -d    delete files that are not on the server (BEWARE!)"
-  echo
-  exit 1
-}
-
-fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-HELP=""
-ARGS=""
-SRC="isabelle-website"
-
-while getopts "hnwd" OPT
-do
-  case "$OPT" in
-    h)
-      HELP=true
-      ;;
-    n)
-      ARGS="$ARGS -n"
-      ;;
-    w)
-      echo "option -w ignored"
-      ;;
-    d)
-      ARGS="$ARGS --delete"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift `expr $OPTIND - 1`
-
-
-# help
-
-if [ -n "$HELP" ]; then
-  cat <<EOF
-
-Mirroring the Isabelle distribution or website
-==============================================
-
-The Munich site maintains an rsync server for the Isabelle
-distribution or website.
-
-The rsync tool is very smart and efficient in mirroring large
-directory hierarchies.  See http://rsync.samba.org/ for more
-information.  The $PRG script provides a simple front-end
-for easy access to the Isabelle distribution.
-
-The script can be either run in conservative or clean-sweep mode.
-
-1) Basic mirroring works like this:
-
-  $PRG /foo/bar
-
-where /foo/bar refers to your local copy of the Isabelle distribution
-(the base directory has to exist already).  This operation is
-conservative in the sense that files are never deleted, thus garbage
-may accumulate over time as our master copy is changed.
-
-Avoiding garbage in your local copy requires some care.  Rsync
-provides a way to delete all additional local files that are absent in
-the master copy.  This provides an efficient way to purge large
-directory hierarchies, even unwillingly in case that a wrong
-destination is given!
-
-2a) This will invoke a safe dry-run of clean-sweep mirroring:
-
-  $PRG -dn /foo/bar
-
-where additions and deletions will be printed without any actual
-changes performed so far.
-
-2b) Exact mirroring with actual deletion of garbage may be performed
-like this:
-
-  $PRG -d /foo/bar
-
-
-After gaining some confidence in the workings of $PRG one
-would usually set up some automatic mirror scheme, e.g. a daily cron
-job run by the 'nobody' user.
-
-Add -w to the option list in order to mirror the whole Isabelle website
-
-EOF
-  exit 0
-fi
-
-
-# arguments
-
-[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
-
-DEST="$1"; shift;
-
-
-## main
-
-exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"