docs: prompts in shell sessions shouldn’t be selectable r/8316

these just indicate the start of the prompt by convention & if the user
is root or not with `#` & `$` respectively

Change-Id: Id65f5f879b067ee96715b3e7dc63f68c7ad791b8
Reviewed-on: https://cl.tvl.fyi/c/depot/+/11868
Reviewed-by: flokli <flokli@flokli.de>
Tested-by: BuildkiteCI

1 files changed, 7 insertions, 0 deletions

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;
+}