proper fonts (cf. 1d219d76873b);
authorwenzelm
Sat, 01 Jul 2017 16:26:15 +0200
changeset 66242 a912f4a701bf
parent 66241 8f39d60b943d
child 66243 453f9cabddb5
proper fonts (cf. 1d219d76873b);
Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Sat Jul 01 16:22:47 2017 +0200
+++ b/Admin/lib/Tools/makedist	Sat Jul 01 16:26:15 2017 +0200
@@ -238,7 +238,7 @@
 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