| changeset 64369 | 6a9816764b37 |
| parent 64221 | 407f69c4959f |
| child 64373 | 5a3e35cb6f54 |
--- a/Admin/lib/Tools/makedist Mon Oct 24 11:48:32 2016 +0200 +++ b/Admin/lib/Tools/makedist Mon Oct 24 12:01:36 2016 +0200 @@ -199,7 +199,7 @@ rm -rf Admin browser_info heaps -./bin/isabelle java isabelle.NEWS +./bin/isabelle news rmdir "$USER_HOME/.isabelle/${DISTNAME}-build" rmdir "$USER_HOME/.isabelle/${DISTNAME}"