style.css | 10 ++++++++++ www.mk | 4 +++- diff --git a/style.css b/style.css new file mode 100644 index 0000000000000000000000000000000000000000..e717af2bcace8146f6ef0a3624599e3993bf07f1a60145fa37cb66314ab52d4a --- /dev/null +++ b/style.css @@ -0,0 +1,10 @@ + diff --git a/www.mk b/www.mk index 8ee295b9027d5bd3da615c721fd7e820ccf4828d916f4f0e4f3bef451a337c61..c9e0b5d85f8cd861f09c8d97f19e242bc1f6fdc993c49345138274f5a007814a 100644 --- a/www.mk +++ b/www.mk @@ -2,10 +2,12 @@ all: pygost.html MAKEINFO ?= makeinfo +CSS != cat style.css + pygost.html: *.texi rm -f pygost.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 \