# HG changeset patch
# User wenzelm
# Date 1498919175 -7200
# Node ID a912f4a701bf7c31ad111a6bfa9eeb2f8f491acc
# Parent  8f39d60b943de62ef99b4737a456660bbf848142
proper fonts (cf. 1d219d76873b);

diff -r 8f39d60b943d -r a912f4a701bf 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