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