Admin/Mercurial/filemap
changeset 28117 83b1f0f7de99
parent 27447 0761334cd591
equal deleted inserted replaced
28116:cd2547ab0696 28117:83b1f0f7de99
     1 rename Doc doc-src
     1 rename Doc doc-src
     2 exclude Distribution/bin/Isabelle
     2 exclude Distribution/bin/Isabelle
       
     3 exclude Admin/page/main-content/PG-preview.mov
       
     4 exclude Admin/website/media/pg_preview.mov
     3 rename Distribution .
     5 rename Distribution .
     4 rename CCL src/CCL
     6 rename CCL src/CCL
     5 rename CTT src/CTT
     7 rename CTT src/CTT
     6 rename Cube src/Cube
     8 rename Cube src/Cube
     7 rename FOL src/FOL
     9 rename FOL src/FOL