author | wenzelm |
Sat, 01 Jul 2017 16:26:15 +0200 | |
changeset 66242 | a912f4a701bf |
parent 66241 | 8f39d60b943d |
child 66243 | 453f9cabddb5 |
--- 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