equal
deleted
inserted
replaced
3 # mirror script for isabelle distribution |
3 # mirror script for isabelle distribution |
4 # |
4 # |
5 # $Id$ |
5 # $Id$ |
6 # |
6 # |
7 |
7 |
8 |
8 ## diagnostics |
9 |
|
10 ## self references |
|
11 |
9 |
12 PRG=`basename "$0"` |
10 PRG=`basename "$0"` |
13 |
|
14 if [ -h "$0" ]; then |
|
15 THIS=`cd \`dirname "$0"\`; cd \`dirname \\\`find "$0" -ls | cut -d ">" -f 2\\\`\`; pwd` |
|
16 else |
|
17 THIS=`cd \`dirname "$0"\`; pwd` |
|
18 fi |
|
19 |
|
20 SUPER=`cd "$THIS/.."; pwd` |
|
21 |
|
22 |
|
23 ## diagnostics |
|
24 |
11 |
25 usage() |
12 usage() |
26 { |
13 { |
27 echo |
14 echo |
28 echo "Usage: $PRG [OPTIONS] [DEST]" |
15 echo "Usage: $PRG [OPTIONS] [DEST]" |
29 echo |
16 echo |
30 echo " Options are:" |
17 echo " Options are:" |
31 echo " -n dry run, don't do anything, just report what would happen" |
18 echo " -n dry run, don't do anything, just report what would happen" |
32 echo " -d delete files that are not on the server" |
19 echo " -d delete files that are not on the server (beware!)" |
33 echo |
20 echo |
34 exit 1 |
21 exit 1 |
35 } |
22 } |
36 |
23 |
37 fail() |
24 fail() |
69 |
56 |
70 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; } |
57 [ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; } |
71 |
58 |
72 DEST="$1"; shift; |
59 DEST="$1"; shift; |
73 |
60 |
|
61 |
74 ## main |
62 ## main |
75 |
63 |
76 rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. $DEST/. |
64 exec rsync -va $ARGS rsync://www4.in.tum.de/isabelle-dist/. "$DEST/." |