From 8334b8359590da3958f36cd0da31b28f1dcd4be1 Mon Sep 17 00:00:00 2001
From: Jan Tojnar <jtojnar@gmail.com>
Date: Tue, 14 Jan 2020 15:04:21 +0100
Subject: [PATCH] doc: Make prompt unselectable

Weirdly, no-one seems to have noticed this was broken.
---
 doc/overrides.css | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/doc/overrides.css b/doc/overrides.css
index 4c7d4a31be2..cc21645a0dd 100644
--- a/doc/overrides.css
+++ b/doc/overrides.css
@@ -7,3 +7,10 @@
 .calloutlist img {
     width: 1.5em;
 }
+
+.prompt {
+    -moz-user-select: none;
+    -webkit-user-select: none;
+    -ms-user-select: none;
+    user-select: none;
+}