From 6dbbd36a817cd0818f3de41eea96ad1e33d3ab6c Mon Sep 17 00:00:00 2001
From: Christian Grothoff <christian@grothoff.org>
Date: Sat, 14 Oct 2017 11:37:03 +0200
Subject: [PATCH] add CSS to dist

---
 doc/Makefile.am | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/doc/Makefile.am b/doc/Makefile.am
index f8c874193..6788a1c84 100644
--- a/doc/Makefile.am
+++ b/doc/Makefile.am
@@ -31,4 +31,7 @@ extra_TEXINFOS = \
 EXTRA_DIST = \
   coding-style.txt \
   $(man_MANS) \
-  $(extra_TEXINFOS)
+  $(extra_TEXINFOS) \
+  docstyle.css \
+  brown-paper.css
+