6.7.3

2026-06-10 20:49:43 +00:00 · 2019-12-17 07:03:06 -05:00
parent 79a34b0d44
commit 17e04d996f
14 changed files with 37 additions and 28 deletions
@@ -672,6 +672,10 @@ div.code-block-caption + div > div.highlight > pre {
    margin-top: 0;
 }

+div.doctest > div.highlight span.gp {  /* gp: Generic.Prompt */
+    user-select: none;
+}
+
 div.code-block-caption span.caption-number {
    padding: 0.1em 0.3em;
    font-style: italic;