diff options
-rw-r--r-- | cfg.mk | 3 | ||||
-rw-r--r-- | doc/Makefile.am | 6 | ||||
-rw-r--r-- | doc/texinfo.css | 44 |
3 files changed, 50 insertions, 3 deletions
@@ -66,7 +66,8 @@ upload: cp $(distdir).tar.gz $(distdir).tar.gz.sig ../releases/gnutls/$(PACKAGE)/ webdocs: - cd doc && ../build-aux/gendocs.sh -o ../$(htmldir)/manual $(PACKAGE) "$(PACKAGE_NAME)" + cd doc && ../build-aux/gendocs.sh --html "--css-include=texinfo.css" \ + -o ../$(htmldir)/manual/ $(PACKAGE) "$(PACKAGE_NAME)" cp -v doc/reference/html/*.html doc/reference/html/*.png doc/reference/html/*.devhelp doc/reference/html/*.css $(htmldir)/reference/ upload-web: diff --git a/doc/Makefile.am b/doc/Makefile.am index 7d1235d..e5e91eb 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -24,11 +24,13 @@ endif EXTRA_DIST = gdoc TODO libtasn1.html libtasn1.ps libtasn1.pdf info_TEXINFOS = libtasn1.texi -libtasn1_TEXINFOS = fdl-1.3.texi gpl-3.0.texi lgpl-2.1.texi $(gdoc_TEXINFOS) +libtasn1_TEXINFOS = fdl-1.3.texi gpl-3.0.texi lgpl-2.1.texi \ + texinfo.css $(gdoc_TEXINFOS) AM_MAKEINFOFLAGS = -I $(top_builddir)/doc TEXI2DVI = texi2dvi $(AM_MAKEINFOFLAGS) -AM_MAKEINFOHTMLFLAGS = $(AM_MAKEINFOFLAGS) --no-split +AM_MAKEINFOHTMLFLAGS = $(AM_MAKEINFOFLAGS) \ + --no-split --number-sections --css-include=texinfo.css dist_man_MANS = $(gdoc_MANS) asn1Parser.1 asn1Coding.1 asn1Decoding.1 diff --git a/doc/texinfo.css b/doc/texinfo.css new file mode 100644 index 0000000..96df89e --- /dev/null +++ b/doc/texinfo.css @@ -0,0 +1,44 @@ +body { + margin: 2%; + padding: 0 5%; + background: #ffffff; +} +h1,h2,h3,h4,h5 { + font-weight: bold; + padding: 5px 5px 5px 5px; + background-color: #c2e0ff; + color: #336699; +} +h1 { + padding: 2em 2em 2em 5%; + color: white; + background: #336699; + text-align: center; + letter-spacing: 3px; +} +h2 { text-decoration: underline; } +pre { + margin: 0 5%; + padding: 0.5em; +} +pre.example { + border: solid 1px; + background: #eeeeff; + padding-bottom: 1em; +} +pre.verbatim { + border: solid 1px gray; + background: white; + padding-bottom: 1em; +} +div.node { + margin: 0 -5% 0 -2%; + padding: 0.5em 0.5em; + margin-top: 0.5em; + margin-bottom: 0.5em; + font-weight: bold; +} +dd, li { + padding-top: 0.1em; + padding-bottom: 0.1em; +} |