author | wenzelm |
Wed, 13 Jan 2016 20:19:49 +0100 | |
changeset 62171 | 46f0dfedf9ef |
parent 62170 | b61c55e4b4b9 |
child 62172 | 7eaeae127955 |
--- a/Admin/lib/Tools/makedist Wed Jan 13 17:05:08 2016 +0100 +++ b/Admin/lib/Tools/makedist Wed Jan 13 20:19:49 2016 +0100 @@ -228,6 +228,7 @@ mkdir "$DISTNAME/doc" mv "${DISTNAME}-old/doc/"*.pdf \ "${DISTNAME}-old/doc/"*.html \ + "${DISTNAME}-old/doc/"*.css \ "${DISTNAME}-old/doc/"*.ttf \ "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"