1 #!/usr/bin/env bash |
|
2 # |
|
3 # mirror script for Isabelle distribution or website |
|
4 |
|
5 |
|
6 ## diagnostics |
|
7 |
|
8 PRG=`basename "$0"` |
|
9 |
|
10 usage() |
|
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 |
|
24 fail() |
|
25 { |
|
26 echo "$1" >&2 |
|
27 exit 2 |
|
28 } |
|
29 |
|
30 |
|
31 ## process command line |
|
32 |
|
33 # options |
|
34 |
|
35 HELP="" |
|
36 ARGS="" |
|
37 SRC="isabelle-website" |
|
38 |
|
39 while getopts "hnwd" OPT |
|
40 do |
|
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 |
|
58 done |
|
59 |
|
60 shift `expr $OPTIND - 1` |
|
61 |
|
62 |
|
63 # help |
|
64 |
|
65 if [ -n "$HELP" ]; then |
|
66 cat <<EOF |
|
67 |
|
68 Mirroring the Isabelle distribution or website |
|
69 ============================================== |
|
70 |
|
71 The Munich site maintains an rsync server for the Isabelle |
|
72 distribution or website. |
|
73 |
|
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. |
|
78 |
|
79 The script can be either run in conservative or clean-sweep mode. |
|
80 |
|
81 1) Basic mirroring works like this: |
|
82 |
|
83 $PRG /foo/bar |
|
84 |
|
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. |
|
89 |
|
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 |
|
94 destination is given! |
|
95 |
|
96 2a) This will invoke a safe dry-run of clean-sweep mirroring: |
|
97 |
|
98 $PRG -dn /foo/bar |
|
99 |
|
100 where additions and deletions will be printed without any actual |
|
101 changes performed so far. |
|
102 |
|
103 2b) Exact mirroring with actual deletion of garbage may be performed |
|
104 like this: |
|
105 |
|
106 $PRG -d /foo/bar |
|
107 |
|
108 |
|
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. |
|
112 |
|
113 Add -w to the option list in order to mirror the whole Isabelle website |
|
114 |
|
115 EOF |
|
116 exit 0 |
|
117 fi |
|
118 |
|
119 |
|
120 # arguments |
|
121 |
|
122 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; } |
|
123 |
|
124 DEST="$1"; shift; |
|
125 |
|
126 |
|
127 ## main |
|
128 |
|
129 exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/" |
|