adding remarks after static inspection of the invocation of the SML code generator
3 # mirror script for Isabelle distribution or website
13 echo "Usage: $PRG [OPTIONS] DEST"
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!)"
31 ## process command line
37 SRC="isabelle-website"
39 while getopts "hnwd" OPT
49 echo "option -w ignored"
60 shift `expr $OPTIND - 1`
65 if [ -n "$HELP" ]; then
68 Mirroring the Isabelle distribution or website
69 ==============================================
71 The Munich site maintains an rsync server for the Isabelle
72 distribution or website.
74 The rsync tool is very smart and efficient in mirroring large
75 directory hierarchies. See http://rsync.samba.org/ for more
76 information. The $PRG script provides a simple front-end
77 for easy access to the Isabelle distribution.
79 The script can be either run in conservative or clean-sweep mode.
81 1) Basic mirroring works like this:
85 where /foo/bar refers to your local copy of the Isabelle distribution
86 (the base directory has to exist already). This operation is
87 conservative in the sense that files are never deleted, thus garbage
88 may accumulate over time as our master copy is changed.
90 Avoiding garbage in your local copy requires some care. Rsync
91 provides a way to delete all additional local files that are absent in
92 the master copy. This provides an efficient way to purge large
93 directory hierarchies, even unwillingly in case that a wrong
96 2a) This will invoke a safe dry-run of clean-sweep mirroring:
100 where additions and deletions will be printed without any actual
101 changes performed so far.
103 2b) Exact mirroring with actual deletion of garbage may be performed
109 After gaining some confidence in the workings of $PRG one
110 would usually set up some automatic mirror scheme, e.g. a daily cron
111 job run by the 'nobody' user.
113 Add -w to the option list in order to mirror the whole Isabelle website
122 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
129 exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"