author | wenzelm |
Mon, 24 Oct 2016 14:37:37 +0200 | |
changeset 64373 | 5a3e35cb6f54 |
parent 64372 | 7ffd2be0a1e8 |
child 64374 | 80d498d56116 |
--- 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" -