From b9b2505e729039a79c0dccf49dcf6af972cff63e Mon Sep 17 00:00:00 2001
From: taoky <me@taoky.moe>
Date: Mon, 18 May 2026 04:02:53 +0800
Subject: [PATCH] feat: Disallow user selection on .highlight .gp

Make copying commands easier
---
 docs/css/extra.css  | 2 ++
 docs/css/extra.scss | 4 ++++
 2 files changed, 6 insertions(+)

diff --git a/docs/css/extra.css b/docs/css/extra.css
index 46b4895f..8685cb1a 100644
--- a/docs/css/extra.css
+++ b/docs/css/extra.css
@@ -47,3 +47,5 @@
 .md-typeset p.caption { text-align: center; font-size: 0.94em; color: grey; margin: -0.7em 0 0; }
 
 .md-typeset .footnote hr { margin-top: 0.2em; }
+
+.highlight .gp { user-select: none; }
diff --git a/docs/css/extra.scss b/docs/css/extra.scss
index ed85485a..9e2ae294 100644
--- a/docs/css/extra.scss
+++ b/docs/css/extra.scss
@@ -97,3 +97,7 @@ $color-codes: red, darkred, orangered, green, limegreen, cyan, darkcyan;
     margin-top: 0.2em;
   }
 }
+
+.highlight .gp {
+  user-select: none;
+}