adjusted sydney to new website
authorhaftmann
Thu Oct 06 08:58:58 2005 +0200 (2005-10-06)
changeset 17770f13472d00645
parent 17769 3a324f3b34f6
child 17771 1e07f6ab3118
adjusted sydney to new website
Admin/mirror-dist
Admin/mirror-main
Admin/rsync-isabelle
     1.1 --- a/Admin/mirror-dist	Thu Oct 06 08:56:15 2005 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,32 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# $Id$
     1.7 -#
     1.8 -# Mirrors the Isabelle distribution pages and downloads. 
     1.9 -#
    1.10 -# It does *not* mirror the home page (those directly on 
    1.11 -# http://isabelle.in.tum.de). There is a separate utility 
    1.12 -# (mirror-main) for that.
    1.13 -#
    1.14 -# Usage: mirror-dist
    1.15 -#
    1.16 -
    1.17 -
    1.18 -HOST=$(hostname)
    1.19 -
    1.20 -case ${HOST} in
    1.21 -  sunbroy*)
    1.22 -    #test
    1.23 -    DEST=/tmp/isabelle-dist
    1.24 -    mkdir -p $DEST
    1.25 -    ;;
    1.26 -  *.cl.cam.ac.uk)
    1.27 -    DEST=/anfs/www/html/Research/HVG/Isabelle/dist
    1.28 -    ;;
    1.29 -  *)
    1.30 -    echo "Unknown destination directory for ${HOST}"
    1.31 -    exit 2
    1.32 -    ;;
    1.33 -esac
    1.34 -
    1.35 -exec $(dirname $0)/rsync-isabelle -d $DEST
     2.1 --- a/Admin/mirror-main	Thu Oct 06 08:56:15 2005 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,34 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# $Id$
     2.7 -#
     2.8 -# Mirrors the Isabelle home page (those directly on http://isabelle.in.tum.de)
     2.9 -# It *does* mirror the Isabelle distribution pages and downloads. There
    2.10 -# is also a separate utility (mirror-dist) for that.
    2.11 -#
    2.12 -# Usage: mirror-main
    2.13 -#
    2.14 -
    2.15 -HOST=$(hostname)
    2.16 -
    2.17 -case ${HOST} in
    2.18 -  sunbroy2)
    2.19 -    DEST=/home/html/isabelle/html-data
    2.20 -    ;;
    2.21 -  atbroy1)
    2.22 -    DEST=/home/html/isabelle/html-data
    2.23 -    ;;
    2.24 -  *.cl.cam.ac.uk)
    2.25 -    USER=paulson
    2.26 -    DEST=/anfs/www/html/Research/HVG/Isabelle
    2.27 -    ;;
    2.28 -  *)
    2.29 -    echo "Unknown destination directory for ${HOST}"
    2.30 -    exit 2
    2.31 -    ;;
    2.32 -esac
    2.33 -
    2.34 -echo "Warning: this script now mirrors the *complete* Isabelle site"
    2.35 -
    2.36 -rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va --copy-links \
    2.37 -  $USER@sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle/website/. $DEST/.
     3.1 --- a/Admin/rsync-isabelle	Thu Oct 06 08:56:15 2005 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,124 +0,0 @@
     3.4 -#!/bin/sh
     3.5 -#
     3.6 -# mirror script for Isabelle distribution
     3.7 -#
     3.8 -# $Id$
     3.9 -#
    3.10 -
    3.11 -## diagnostics
    3.12 -
    3.13 -PRG=`basename "$0"`
    3.14 -
    3.15 -usage()
    3.16 -{
    3.17 -  echo
    3.18 -  echo "Usage: $PRG [OPTIONS] DEST"
    3.19 -  echo
    3.20 -  echo "  Options are:"
    3.21 -  echo "    -h    print help message"
    3.22 -  echo "    -n    dry run, don't do anything, just report what would happen"
    3.23 -  echo "    -d    delete files that are not on the server (BEWARE!)"
    3.24 -  echo
    3.25 -  exit 1
    3.26 -}
    3.27 -
    3.28 -fail()
    3.29 -{
    3.30 -  echo "$1" >&2
    3.31 -  exit 2
    3.32 -}
    3.33 -
    3.34 -
    3.35 -## process command line
    3.36 -
    3.37 -# options
    3.38 -
    3.39 -HELP=""
    3.40 -ARGS=""
    3.41 -
    3.42 -while getopts "hnd" OPT
    3.43 -do
    3.44 -  case "$OPT" in
    3.45 -    h)
    3.46 -      HELP=true
    3.47 -      ;;
    3.48 -    n)
    3.49 -      ARGS="$ARGS -n"
    3.50 -      ;;
    3.51 -    d)
    3.52 -      ARGS="$ARGS --delete"
    3.53 -      ;;
    3.54 -    \?)
    3.55 -      usage
    3.56 -      ;;
    3.57 -  esac
    3.58 -done
    3.59 -
    3.60 -shift `expr $OPTIND - 1`
    3.61 -
    3.62 -
    3.63 -# help
    3.64 -
    3.65 -if [ -n "$HELP" ]; then
    3.66 -  cat <<EOF
    3.67 -
    3.68 -Mirroring the Isabelle Distribution
    3.69 -===================================
    3.70 -
    3.71 -The Munich site maintains an rsync server for the Isabelle
    3.72 -distribution, including complete sources, binaries, and documentation.
    3.73 -
    3.74 -The rsync tool is very smart and efficient in mirroring large
    3.75 -directory hierarchies.  See http://rsync.samba.org/ for more
    3.76 -information.  The rsync-isabelle script provides a simple front-end
    3.77 -for easy access to the Isabelle distribution.
    3.78 -
    3.79 -The script can be either run in conservative or clean-sweep mode.
    3.80 -
    3.81 -1) Basic mirroring works like this:
    3.82 -
    3.83 -  ./rsync-isabelle /foo/bar
    3.84 -
    3.85 -where /foo/bar refers to your local copy of the Isabelle distribution
    3.86 -(the base directory has to exist already).  This operation is
    3.87 -conservative in the sense that files are never deleted, thus garbage
    3.88 -may accumulate over time as our master copy is changed.
    3.89 -
    3.90 -Avoiding garbage in your local copy requires some care.  Rsync
    3.91 -provides a way to delete all additional local files that are absent in
    3.92 -the master copy.  This provides an efficient way to purge large
    3.93 -directory hierarchies, even unwillingly in case that a wrong
    3.94 -destination is given!
    3.95 -
    3.96 -2a) This will invoke a safe dry-run of clean-sweep mirroring:
    3.97 -
    3.98 -  ./rsync-isabelle -dn /foo/bar
    3.99 -
   3.100 -where additions and deletions will be printed without any actual
   3.101 -changes performed so far.
   3.102 -
   3.103 -2b) Exact mirroring with actual deletion of garbage may be performed
   3.104 -like this:
   3.105 -
   3.106 -  ./rsync-isabelle -d /foo/bar
   3.107 -
   3.108 -
   3.109 -After gaining some confidence in the workings of rsync-isabelle one
   3.110 -would usually set up some automatic mirror scheme, e.g. a daily cron
   3.111 -job run by the 'nobody' user.
   3.112 -
   3.113 -EOF
   3.114 -  exit 0
   3.115 -fi
   3.116 -
   3.117 -
   3.118 -# arguments
   3.119 -
   3.120 -[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
   3.121 -
   3.122 -DEST="$1"; shift;
   3.123 -
   3.124 -
   3.125 -## main
   3.126 -
   3.127 -exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/."