Admin/lib/Tools/makedist
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"
-