Admin/lib/Tools/makedist

 mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
   "${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/Contents" "$DISTNAME/doc"
 
 rm -f Isabelle && ln -sf "$DISTNAME" Isabelle