add CSS to dist

This commit is contained in:
Christian Grothoff 2017-10-14 11:37:03 +02:00
parent b5f5956ee2
commit 6dbbd36a81
No known key found for this signature in database
GPG Key ID: 939E6BE1E29FC3CC

View File

@ -31,4 +31,7 @@ extra_TEXINFOS = \
EXTRA_DIST = \ EXTRA_DIST = \
coding-style.txt \ coding-style.txt \
$(man_MANS) \ $(man_MANS) \
$(extra_TEXINFOS) $(extra_TEXINFOS) \
docstyle.css \
brown-paper.css