exclude large .mov files;
authorwenzelm
Wed, 03 Sep 2008 19:52:45 +0200
changeset 28117 83b1f0f7de99
parent 28116 cd2547ab0696
child 28118 c21ac4bd18a9
exclude large .mov files;
Admin/Mercurial/filemap
--- a/Admin/Mercurial/filemap	Wed Sep 03 17:50:37 2008 +0200
+++ b/Admin/Mercurial/filemap	Wed Sep 03 19:52:45 2008 +0200
@@ -1,5 +1,7 @@
 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