Commit Graph

8 Commits

Author SHA1 Message Date
github-actions[bot]
682c71855c
Revert "manual: fold sidebar sections" (#10700)
(cherry picked from commit 937e7bae48)

Co-authored-by: Valentin Gagarin <valentin.gagarin@tweag.io>
2024-05-15 22:40:57 +02:00
Valentin Gagarin
140de3b278 manual: fold sidebar sections
the table of contents is very long now, and folded sections allow
for a better overview.
2024-02-08 09:00:00 +01: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