isabelle: Admin/Mercurial/convert@dd02201d95b6 (annotated)

27444 a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	1	#!/bin/bash
a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	2	# $Id$
a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	3
a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	4	THIS="$(cd "$(dirname "$0")"; pwd)"
a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	5	SUPER="$(cd "$THIS/.."; pwd)"
a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	6
27462 53a350398593 output to log file; wenzelm parents: 27459 diff changeset	7	LOG="$THIS/log"
27465 79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	8	date >> "$LOG"
79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	9
79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	10
79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	11	## cvs update
27462 53a350398593 output to log file; wenzelm parents: 27459 diff changeset	12
27444 a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	13	cd "$THIS/cvs"
27463 9971758c50be redirect stderr as well; wenzelm parents: 27462 diff changeset	14	cvs up -dAP >> "$LOG" 2>&1 \|\| exit 2
27444 a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	15
a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	16
27465 79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	17	## hg convert
79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	18
27457 a701c0b951d8 provide HGRCPATH, taken from cvs/Admin; wenzelm parents: 27444 diff changeset	19	export HGRCPATH="$THIS/cvs/Admin/Mercurial/hgrc"
a701c0b951d8 provide HGRCPATH, taken from cvs/Admin; wenzelm parents: 27444 diff changeset	20
27444 a487aa892540 convert Isabelle CVS to Mercurial; wenzelm parents: diff changeset	21	cd "$THIS"
28929 32831901e1ae convert to isabelle-cvs, the old version; wenzelm parents: 28118 diff changeset	22	/home/isabelle/mercurial/bin/hg convert --filemap cvs/Admin/Mercurial/filemap cvs isabelle-cvs >> "$LOG" 2>&1 \|\| exit 2
27459 62bab1679283 ensure hg/.hg/hgrc; wenzelm parents: 27457 diff changeset	23
28929 32831901e1ae convert to isabelle-cvs, the old version; wenzelm parents: 28118 diff changeset	24	[ -e isabelle-cvs/.hg/hgrc ] \|\| ln -s ../../cvs/Admin/Mercurial/hgrc isabelle-cvs/.hg/hgrc
27464 3640865d4a38 logrotate setup; wenzelm parents: 27463 diff changeset	25
3640865d4a38 logrotate setup; wenzelm parents: 27463 diff changeset	26
27465 79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	27	## logrotate
79db00d0fba9 tuned; wenzelm parents: 27464 diff changeset	28
27464 3640865d4a38 logrotate setup; wenzelm parents: 27463 diff changeset	29	/usr/sbin/logrotate -s "$THIS/log.state" "$THIS/cvs/Admin/Mercurial/logrotate.conf"

author	huffman
	Mon, 01 Mar 2010 16:36:25 -0800
changeset 35489	dd02201d95b6
parent 28929	32831901e1ae
permissions	-rwxr-xr-x