# HG changeset patch
# User wenzelm
# Date 1452697263 -3600
# Node ID cb806a024bba4954d90ccd4d8ec92b63a1d0716d
# Parent  3499ec79ad4b79f681d5867d55ab21de2813b797
more doc content;

diff -r 3499ec79ad4b -r cb806a024bba Admin/lib/Tools/makedist
--- 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