Updated HTML docs

This commit is contained in:
Griatch 2021-11-10 01:28:35 +01:00
parent 655de3b654
commit e997b9b8a2
53 changed files with 249 additions and 236 deletions

View file

@ -696,6 +696,12 @@ div.code-block-caption + div > div.highlight > pre {
margin-top: 0;
}
div.highlight > pre {
font-family: "Ubuntu Mono", monospace;
line-height: 1.4em;
font-size: small;
}
div.doctest > div.highlight span.gp { /* gp: Generic.Prompt */
user-select: none;
}