# HG changeset patch
# User wenzelm
# Date 1220464365 -7200
# Node ID 83b1f0f7de99c3b87fb508fb9ea2cb678dcc4d65
# Parent  cd2547ab0696cf3d6b6405cf9b9e454a37027e83
exclude large .mov files;

diff -r cd2547ab0696 -r 83b1f0f7de99 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