Admin/lib/Tools/makedist

   "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
 mkdir "$DISTNAME/doc"
 mv "${DISTNAME}-old/doc/"*.pdf \
   "${DISTNAME}-old/doc/"*.html \
   "${DISTNAME}-old/doc/"*.css \
-  "${DISTNAME}-old/doc/"*.ttf \
+  "${DISTNAME}-old/doc/fonts" \
   "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
 
 rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
 
 rm -rf "${DISTNAME}-old"