--- a/Admin/lib/Tools/makedist Wed Jan 13 15:59:37 2016 +0100
+++ b/Admin/lib/Tools/makedist Wed Jan 13 16:01:03 2016 +0100
@@ -226,7 +226,10 @@
mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
"${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
mkdir "$DISTNAME/doc"
-mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
+mv "${DISTNAME}-old/doc/"*.pdf \
+ "${DISTNAME}-old/doc/"*.html \
+ "${DISTNAME}-old/doc/"*.ttf \
+ "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
rm -f Isabelle && ln -sf "$DISTNAME" Isabelle