about summary refs log tree commit diff
diff options
context:
space:
mode:
-rw-r--r--tvix/docs/book.toml2
-rw-r--r--tvix/docs/mdbook-extra.css7
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;
+}