# HG changeset patch
# User wenzelm
# Date 1215023466 -7200
# Node ID 0761334cd591630b208dcb451d3025c2be63d305
# Parent  bac210482607c964304b75a069bfe3ce6c360673
rename Doc doc-src;

diff -r bac210482607 -r 0761334cd591 Admin/Mercurial/filemap
--- a/Admin/Mercurial/filemap	Wed Jul 02 20:13:32 2008 +0200
+++ b/Admin/Mercurial/filemap	Wed Jul 02 20:31:06 2008 +0200
@@ -1,3 +1,4 @@
+rename Doc doc-src
 exclude Distribution/bin/Isabelle
 rename Distribution .
 rename CCL src/CCL