Website restyling

diff --git a/style.css b/style.css
new file mode 100644 (file)
index 0000000..e05fd44
--- /dev/null
+++ b/style.css
@@ -0,0 +1,10 @@
+<style type="text/css"><!--
+body {
+    margin: auto;
+    width: 80em;
+    background-color: #AEBECE;
+}
+h1, h2, h3, h4 { text-align: center }
+h1, h2, h3, h4, strong { color: #900090 }
+pre { background-color: #CCCCCC }
+--></style>

diff --git a/www.mk b/www.mk
index 005d4a8f5b3f8248096a44c0ee50b4fd519d98e7..0670ffdc5077177570a546b3836293d6fa0c3fd2 100644 (file)
--- a/www.mk
+++ b/www.mk
@@ -2,10 +2,12 @@ all: gogost.html
 
 MAKEINFO ?= makeinfo
 
+CSS != cat style.css
+
 gogost.html: *.texi
        rm -f gogost.html/*.html
        $(MAKEINFO) --html \
-               --set-customization-variable NO_CSS=1 \
+               --set-customization-variable CSS_LINES='$(CSS)' \
                --set-customization-variable SHOW_TITLE=0 \
                --set-customization-variable USE_ACCESSKEY=0 \
                --set-customization-variable DATE_IN_HEADER=1 \