Admin/lib/Tools/makedist
changeset 53208 bec95e287d26
parent 51073 a25b899a649d
child 53436 ef2bb63583ac
--- a/Admin/lib/Tools/makedist	Mon Aug 26 16:13:20 2013 +0200
+++ b/Admin/lib/Tools/makedist	Mon Aug 26 16:51:53 2013 +0200
@@ -176,11 +176,11 @@
 
 cp -a src src.orig
 env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
-  ./bin/isabelle build_doc $JOBS -a || fail "Failed to build documentation"
+  ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
 rm -rf src
 mv src.orig src
 
-rm -rf Admin
+rm -rf Admin browser_info heaps
 
 
 # create archive