diff options
Diffstat (limited to 'tvix/docs')
| -rw-r--r-- | tvix/docs/book.toml | 2 | ||||
| -rw-r--r-- | tvix/docs/mdbook-extra.css | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/tvix/docs/book.toml b/tvix/docs/book.toml index a5dacc46ed69..093b73b8e820 100644 --- a/tvix/docs/book.toml +++ b/tvix/docs/book.toml @@ -22,4 +22,4 @@ after = ["links"] # ensure `{{#include}}` also gets processed [output] [output.html] -additional-css = ["./mdbook-admonish.css"] +additional-css = ["./mdbook-admonish.css", "./mdbook-extra.css"] diff --git a/tvix/docs/mdbook-extra.css b/tvix/docs/mdbook-extra.css new file mode 100644 index 000000000000..7a50fdbeed68 --- /dev/null +++ b/tvix/docs/mdbook-extra.css @@ -0,0 +1,7 @@ +@charset "utf-8"; + +.hljs-meta.prompt_ { + -webkit-user-select: none; + -moz-user-select: none; + user-select: none; +} |