Commit graph

7 commits

Author SHA1 Message Date
Qyriad c21d11ac09 docs: replace sed invocation with an mdbook preprocessor for @docroot@
We're not entirely clear on why the links preprocessor has to be done
*before* rather than after, but we assume it is probably that as a
builtin preprocessor it does some processing on the raw book source,
and not just the JSON data.

Also a real use for Python pattern matching? I know I was surprised too.

Change-Id: Ibe8b59e7b5bd5f357a655d8b4c5f0b0f58a67d6b
2024-04-04 21:43:19 +00:00
Robert Hensing be10c09d23 manual: Check links
mdbook-linkcheck is not consistent about its warning setting.
It disables some warnings, but not the warnings about lack of
fragment checking support; hence the extra filtering.
2023-01-10 22:30:41 +01:00
Robert Hensing 1437582ccd
doc/book.toml: Improve config (#7300)
* doc/book.toml: Improve config

 - `title` value will be added to the HTML <title> - here</title>

 - `git-repository-url` adds a link to the GitHub repo in the top right corner

 - `edit-url-template` adds an edit link, inviting contributions

Co-authored-by: Valentin Gagarin <valentin.gagarin@tweag.io>
2022-12-20 16:29:32 +01:00
Jan Tojnar 26d1877d6e doc: Add redirects for the DocBook manual
There are still many links to the old manual on the web and
having them end up on the Introduction page is a bad user experience.
2022-05-26 18:17:21 +02:00
Jan Tojnar 3272afa17b doc: Port anchors preprocessor to jq script
Python is only pulled into the build closure by Mercurial, which might end up being removed.
Let’s port the script to jq, which is more likely to stay.
2022-05-26 18:17:21 +02:00
Jan Tojnar 4de84e095d doc: Introduce pre-processor for adding anchors to text
It is now possible to use the following syntax to insert anchors into the text:

    []{#anchor-name}

The anchor will allow linking to the location it is placed by appending #anchor-name to the URL.

Additionally, it is possible to create a link pointing to its own location by adding text between the square brackets:

    [`--add-root`]{#opt-add-root}
2022-05-26 17:54:15 +02:00
Eelco Dolstra 8a97b11374
Improve margins between sections
The default CSS puts almost no space between sections, but a lot of
space between subsections. This flips that around.
2020-08-19 12:31:18 +02:00