1#!/usr/bin/env bash 2# 3# mirror script for Isabelle distribution or website 4 5 6## diagnostics 7 8PRG=`basename "$0"` 9 10usage() 11{ 12 echo 13 echo "Usage: $PRG [OPTIONS] DEST" 14 echo 15 echo " Options are:" 16 echo " -h print help message" 17 echo " -n dry run, don't do anything, just report what would happen" 18 echo " -w (ignored for backward compatibility)" 19 echo " -d delete files that are not on the server (BEWARE!)" 20 echo 21 exit 1 22} 23 24fail() 25{ 26 echo "$1" >&2 27 exit 2 28} 29 30 31## process command line 32 33# options 34 35HELP="" 36ARGS="" 37SRC="isabelle-website" 38 39while getopts "hnwd" OPT 40do 41 case "$OPT" in 42 h) 43 HELP=true 44 ;; 45 n) 46 ARGS="$ARGS -n" 47 ;; 48 w) 49 echo "option -w ignored" 50 ;; 51 d) 52 ARGS="$ARGS --delete" 53 ;; 54 \?) 55 usage 56 ;; 57 esac 58done 59 60shift `expr $OPTIND - 1` 61 62 63# help 64 65if [ -n "$HELP" ]; then 66 cat <<EOF 67 68Mirroring the Isabelle distribution or website 69============================================== 70 71The Munich site maintains an rsync server for the Isabelle 72distribution or website. 73 74The rsync tool is very smart and efficient in mirroring large 75directory hierarchies. See http://rsync.samba.org/ for more 76information. The $PRG script provides a simple front-end 77for easy access to the Isabelle distribution. 78 79The script can be either run in conservative or clean-sweep mode. 80 811) Basic mirroring works like this: 82 83 $PRG /foo/bar 84 85where /foo/bar refers to your local copy of the Isabelle distribution 86(the base directory has to exist already). This operation is 87conservative in the sense that files are never deleted, thus garbage 88may accumulate over time as our master copy is changed. 89 90Avoiding garbage in your local copy requires some care. Rsync 91provides a way to delete all additional local files that are absent in 92the master copy. This provides an efficient way to purge large 93directory hierarchies, even unwillingly in case that a wrong 94destination is given! 95 962a) This will invoke a safe dry-run of clean-sweep mirroring: 97 98 $PRG -dn /foo/bar 99 100where additions and deletions will be printed without any actual 101changes performed so far. 102 1032b) Exact mirroring with actual deletion of garbage may be performed 104like this: 105 106 $PRG -d /foo/bar 107 108 109After gaining some confidence in the workings of $PRG one 110would usually set up some automatic mirror scheme, e.g. a daily cron 111job run by the 'nobody' user. 112 113Add -w to the option list in order to mirror the whole Isabelle website 114 115EOF 116 exit 0 117fi 118 119 120# arguments 121 122[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; } 123 124DEST="$1"; shift; 125 126 127## main 128 129exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/" 130