From 8a97b11374c5165d3602648c5c0327f103072105 Mon Sep 17 00:00:00 2001
From: Eelco Dolstra <edolstra@gmail.com>
Date: Wed, 19 Aug 2020 12:31:18 +0200
Subject: [PATCH] Improve margins between sections
The default CSS puts almost no space between sections, but a lot of
space between subsections. This flips that around.
---
doc/manual/book.toml | 2 ++
doc/manual/custom.css | 7 +++++++
doc/manual/local.mk | 2 +-
3 files changed, 10 insertions(+), 1 deletion(-)
create mode 100644 doc/manual/book.toml
create mode 100644 doc/manual/custom.css
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
--
GitLab