diff options
| author | Eelco Dolstra <edolstra@gmail.com> | 2020-08-19 12:31:18 +0200 |
|---|---|---|
| committer | Eelco Dolstra <edolstra@gmail.com> | 2020-08-19 12:31:18 +0200 |
| commit | 8a97b11374c5165d3602648c5c0327f103072105 (patch) | |
| tree | 18f702d63d18c3e85ed76a72d5bb87bdbb1cf9a0 | |
| parent | 069340179e91202b2d3adc5ea1e3023ba2a51691 (diff) | |
Improve margins between sections
The default CSS puts almost no space between sections, but a lot of
space between subsections. This flips that around.
| -rw-r--r-- | doc/manual/book.toml | 2 | ||||
| -rw-r--r-- | doc/manual/custom.css | 7 | ||||
| -rw-r--r-- | doc/manual/local.mk | 2 |
3 files changed, 10 insertions, 1 deletions
diff --git a/doc/manual/book.toml b/doc/manual/book.toml new file mode 100644 index 000000000..fee41dfb3 --- /dev/null +++ b/doc/manual/book.toml @@ -0,0 +1,2 @@ +[output.html] +additional-css = ["custom.css"] diff --git a/doc/manual/custom.css b/doc/manual/custom.css new file mode 100644 index 000000000..69d48d4a7 --- /dev/null +++ b/doc/manual/custom.css @@ -0,0 +1,7 @@ +h1:not(:first-of-type) { + margin-top: 1.3em; +} + +h2 { + margin-top: 1em; +} diff --git a/doc/manual/local.mk b/doc/manual/local.mk index 8f917316d..04c57b23b 100644 --- a/doc/manual/local.mk +++ b/doc/manual/local.mk @@ -33,7 +33,7 @@ $(d)/nix.json: $(bindir)/nix # Generate the HTML manual. install: $(docdir)/manual/index.html -$(docdir)/manual/index.html: $(MANUAL_SRCS) +$(docdir)/manual/index.html: $(MANUAL_SRCS) $(d)/book.toml $(d)/custom.css $(trace-gen) mdbook build doc/manual -d $(docdir)/manual @cp doc/manual/highlight.pack.js $(docdir)/manual/highlight.js |