# 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