equal
deleted
inserted
replaced
1 #!/bin/bash |
|
2 # $Id$ |
|
3 |
|
4 THIS="$(cd "$(dirname "$0")"; pwd)" |
|
5 SUPER="$(cd "$THIS/.."; pwd)" |
|
6 |
|
7 LOG="$THIS/log" |
|
8 date >> "$LOG" |
|
9 |
|
10 |
|
11 ## cvs update |
|
12 |
|
13 cd "$THIS/cvs" |
|
14 cvs up -dAP >> "$LOG" 2>&1 || exit 2 |
|
15 |
|
16 |
|
17 ## hg convert |
|
18 |
|
19 export HGRCPATH="$THIS/cvs/Admin/Mercurial/hgrc" |
|
20 |
|
21 cd "$THIS" |
|
22 /home/isabelle/mercurial/bin/hg convert --filemap cvs/Admin/Mercurial/filemap cvs isabelle-cvs >> "$LOG" 2>&1 || exit 2 |
|
23 |
|
24 [ -e isabelle-cvs/.hg/hgrc ] || ln -s ../../cvs/Admin/Mercurial/hgrc isabelle-cvs/.hg/hgrc |
|
25 |
|
26 |
|
27 ## logrotate |
|
28 |
|
29 /usr/sbin/logrotate -s "$THIS/log.state" "$THIS/cvs/Admin/Mercurial/logrotate.conf" |
|