diff options
| -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 |