5 # mirror script for Isabelle distribution or website
15 echo "Usage: $PRG [OPTIONS] DEST"
18 echo " -h print help message"
19 echo " -n dry run, don't do anything, just report what would happen"
20 echo " -w (ignored for backward compatibility)"
21 echo " -d delete files that are not on the server (BEWARE!)"
33 ## process command line
39 SRC="isabelle-website"
41 while getopts "hnwd" OPT
51 echo "option -w ignored"
62 shift `expr $OPTIND - 1`
67 if [ -n "$HELP" ]; then
70 Mirroring the Isabelle distribution or website
71 ==============================================
73 The Munich site maintains an rsync server for the Isabelle
74 distribution or website.
76 The rsync tool is very smart and efficient in mirroring large
77 directory hierarchies. See http://rsync.samba.org/ for more
78 information. The $PRG script provides a simple front-end
79 for easy access to the Isabelle distribution.
81 The script can be either run in conservative or clean-sweep mode.
83 1) Basic mirroring works like this:
87 where /foo/bar refers to your local copy of the Isabelle distribution
88 (the base directory has to exist already). This operation is
89 conservative in the sense that files are never deleted, thus garbage
90 may accumulate over time as our master copy is changed.
92 Avoiding garbage in your local copy requires some care. Rsync
93 provides a way to delete all additional local files that are absent in
94 the master copy. This provides an efficient way to purge large
95 directory hierarchies, even unwillingly in case that a wrong
98 2a) This will invoke a safe dry-run of clean-sweep mirroring:
102 where additions and deletions will be printed without any actual
103 changes performed so far.
105 2b) Exact mirroring with actual deletion of garbage may be performed
111 After gaining some confidence in the workings of $PRG one
112 would usually set up some automatic mirror scheme, e.g. a daily cron
113 job run by the 'nobody' user.
115 Add -w to the option list in order to mirror the whole Isabelle website
124 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
131 exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"