changeset 64373 | 5a3e35cb6f54 |
parent 64369 | 6a9816764b37 |
child 64404 | d75397e0aad5 |
--- a/Admin/lib/Tools/makedist Mon Oct 24 14:10:53 2016 +0200 +++ b/Admin/lib/Tools/makedist Mon Oct 24 14:37:37 2016 +0200 @@ -197,9 +197,9 @@ rm -rf src mv src.orig src -rm -rf Admin browser_info heaps +./bin/isabelle news -./bin/isabelle news +rm -rf Admin browser_info heaps rmdir "$USER_HOME/.isabelle/${DISTNAME}-build" rmdir "$USER_HOME/.isabelle/${DISTNAME}" @@ -244,4 +244,3 @@ rm -f Isabelle && ln -sf "$DISTNAME" Isabelle rm -rf "${DISTNAME}-old" -