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