diff -r 8160596aeb65 -r d7085f0ec087 Admin/Mercurial/convert
--- a/Admin/Mercurial/convert	Wed May 12 15:31:43 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-#!/bin/bash
-# $Id$
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-SUPER="$(cd "$THIS/.."; pwd)"
-
-LOG="$THIS/log"
-date >> "$LOG"
-
-
-## cvs update
-
-cd "$THIS/cvs"
-cvs up -dAP >> "$LOG" 2>&1 || exit 2
-
-
-## hg convert
-
-export HGRCPATH="$THIS/cvs/Admin/Mercurial/hgrc"
-
-cd "$THIS"
-/home/isabelle/mercurial/bin/hg convert --filemap cvs/Admin/Mercurial/filemap cvs isabelle-cvs >> "$LOG" 2>&1 || exit 2
-
-[ -e isabelle-cvs/.hg/hgrc ] || ln -s ../../cvs/Admin/Mercurial/hgrc isabelle-cvs/.hg/hgrc
-
-
-## logrotate
-
-/usr/sbin/logrotate -s "$THIS/log.state" "$THIS/cvs/Admin/Mercurial/logrotate.conf"