author | wenzelm |
Sat, 29 Nov 2008 19:21:32 +0100 | |
changeset 28912 | ddbadafef6bd |
parent 28911 | 88193464e443 |
child 28913 | 86ed1c86e0ef |
--- a/Admin/makedist_mercurial Sat Nov 29 19:20:12 2008 +0100 +++ b/Admin/makedist_mercurial Sat Nov 29 19:21:32 2008 +0100 @@ -98,6 +98,8 @@ rm -f "isabelle-$IDENT/.hg_archival.txt" rm -f "isabelle-$IDENT/.hgtags" +rm -f "isabelle-$IDENT/.hgignore" +rm -f "isabelle-$IDENT/README_REPOSITORY" # dist name