diff -r b78d3c87fc88 -r f99ae7e27150 Admin/Mercurial/filemap
--- a/Admin/Mercurial/filemap	Wed May 12 15:25:23 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-rename Doc doc-src
-exclude Distribution/bin/Isabelle
-exclude Admin/page/main-content/PG-preview.mov
-exclude Admin/website/media/pg_preview.mov
-rename Distribution .
-rename CCL src/CCL
-rename CTT src/CTT
-rename Cube src/Cube
-rename FOL src/FOL
-rename FOLP src/FOLP
-rename HOL src/HOL
-rename HOLCF src/HOLCF
-rename LCF src/LCF
-rename LK src/LK
-rename Modal src/Modal
-rename Provers src/Provers
-rename Pure src/Pure
-rename Sequents src/Sequents
-rename Tools src/Tools
-rename ZF src/ZF