# HG changeset patch
# User haftmann
# Date 1128581938 -7200
# Node ID f13472d00645e9469529b5bde02f2482247f8c58
# Parent  3a324f3b34f675c41e8f474118a4226d01f72054
adjusted sydney to new website

diff -r 3a324f3b34f6 -r f13472d00645 Admin/mirror-dist
--- a/Admin/mirror-dist	Thu Oct 06 08:56:15 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-#
-# Mirrors the Isabelle distribution pages and downloads. 
-#
-# It does *not* mirror the home page (those directly on 
-# http://isabelle.in.tum.de). There is a separate utility 
-# (mirror-main) for that.
-#
-# Usage: mirror-dist
-#
-
-
-HOST=$(hostname)
-
-case ${HOST} in
-  sunbroy*)
-    #test
-    DEST=/tmp/isabelle-dist
-    mkdir -p $DEST
-    ;;
-  *.cl.cam.ac.uk)
-    DEST=/anfs/www/html/Research/HVG/Isabelle/dist
-    ;;
-  *)
-    echo "Unknown destination directory for ${HOST}"
-    exit 2
-    ;;
-esac
-
-exec $(dirname $0)/rsync-isabelle -d $DEST
diff -r 3a324f3b34f6 -r f13472d00645 Admin/mirror-main
--- a/Admin/mirror-main	Thu Oct 06 08:56:15 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-#!/usr/bin/env bash
-#
-# $Id$
-#
-# Mirrors the Isabelle home page (those directly on http://isabelle.in.tum.de)
-# It *does* mirror the Isabelle distribution pages and downloads. There
-# is also a separate utility (mirror-dist) for that.
-#
-# Usage: mirror-main
-#
-
-HOST=$(hostname)
-
-case ${HOST} in
-  sunbroy2)
-    DEST=/home/html/isabelle/html-data
-    ;;
-  atbroy1)
-    DEST=/home/html/isabelle/html-data
-    ;;
-  *.cl.cam.ac.uk)
-    USER=paulson
-    DEST=/anfs/www/html/Research/HVG/Isabelle
-    ;;
-  *)
-    echo "Unknown destination directory for ${HOST}"
-    exit 2
-    ;;
-esac
-
-echo "Warning: this script now mirrors the *complete* Isabelle site"
-
-rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va --copy-links \
-  $USER@sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle/website/. $DEST/.
diff -r 3a324f3b34f6 -r f13472d00645 Admin/rsync-isabelle
--- a/Admin/rsync-isabelle	Thu Oct 06 08:56:15 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,124 +0,0 @@
-#!/bin/sh
-#
-# mirror script for Isabelle distribution
-#
-# $Id$
-#
-
-## 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 "    -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=""
-
-while getopts "hnd" OPT
-do
-  case "$OPT" in
-    h)
-      HELP=true
-      ;;
-    n)
-      ARGS="$ARGS -n"
-      ;;
-    d)
-      ARGS="$ARGS --delete"
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift `expr $OPTIND - 1`
-
-
-# help
-
-if [ -n "$HELP" ]; then
-  cat <<EOF
-
-Mirroring the Isabelle Distribution
-===================================
-
-The Munich site maintains an rsync server for the Isabelle
-distribution, including complete sources, binaries, and documentation.
-
-The rsync tool is very smart and efficient in mirroring large
-directory hierarchies.  See http://rsync.samba.org/ for more
-information.  The rsync-isabelle 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:
-
-  ./rsync-isabelle /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:
-
-  ./rsync-isabelle -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:
-
-  ./rsync-isabelle -d /foo/bar
-
-
-After gaining some confidence in the workings of rsync-isabelle one
-would usually set up some automatic mirror scheme, e.g. a daily cron
-job run by the 'nobody' user.
-
-EOF
-  exit 0
-fi
-
-
-# arguments
-
-[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
-
-DEST="$1"; shift;
-
-
-## main
-
-exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."