equal
deleted
inserted
replaced
|
1 #!/bin/sh |
|
2 # |
|
3 # mirror script for isabelle distribution |
|
4 # |
|
5 # $Id$ |
|
6 # |
|
7 |
|
8 ## diagnostics |
|
9 |
|
10 PRG=`basename "$0"` |
|
11 |
|
12 usage() |
|
13 { |
|
14 echo |
|
15 echo "Usage: $PRG [OPTIONS] [DEST]" |
|
16 echo |
|
17 echo " Options are:" |
|
18 echo " -n dry run, don't do anything, just report what would happen" |
|
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 ARGS="" |
|
36 |
|
37 while getopts "nd" OPT |
|
38 do |
|
39 case "$OPT" in |
|
40 n) |
|
41 ARGS="$ARGS -n" |
|
42 ;; |
|
43 d) |
|
44 ARGS="$ARGS --delete" |
|
45 ;; |
|
46 \?) |
|
47 usage |
|
48 ;; |
|
49 esac |
|
50 done |
|
51 |
|
52 shift `expr $OPTIND - 1` |
|
53 |
|
54 |
|
55 # arguments |
|
56 |
|
57 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; } |
|
58 |
|
59 DEST="$1"; shift; |
|
60 |
|
61 |
|
62 ## main |
|
63 |
|
64 exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/." |