Admin/lib/Tools/makedist
changeset 64373 5a3e35cb6f54
parent 64369 6a9816764b37
child 64404 d75397e0aad5
     1.1 --- a/Admin/lib/Tools/makedist	Mon Oct 24 14:10:53 2016 +0200
     1.2 +++ b/Admin/lib/Tools/makedist	Mon Oct 24 14:37:37 2016 +0200
     1.3 @@ -197,9 +197,9 @@
     1.4  rm -rf src
     1.5  mv src.orig src
     1.6  
     1.7 -rm -rf Admin browser_info heaps
     1.8 +./bin/isabelle news
     1.9  
    1.10 -./bin/isabelle news
    1.11 +rm -rf Admin browser_info heaps
    1.12  
    1.13  rmdir "$USER_HOME/.isabelle/${DISTNAME}-build"
    1.14  rmdir "$USER_HOME/.isabelle/${DISTNAME}"
    1.15 @@ -244,4 +244,3 @@
    1.16  rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
    1.17  
    1.18  rm -rf "${DISTNAME}-old"
    1.19 -