From 3b6599b12470fe9b1321111d31c34685ffd5db52 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Mon, 24 Jan 2022 18:12:13 -0500 Subject: Github doesn't remove Unicode letters from header slugs apparently --- docs/help/first_pick.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'docs/help/first_pick.html') diff --git a/docs/help/first_pick.html b/docs/help/first_pick.html index e2d98d30..1e70daf4 100644 --- a/docs/help/first_pick.html +++ b/docs/help/first_pick.html @@ -5,7 +5,7 @@

Square Image Of Or Equal To ()

-

𝕩: First

+

𝕩: First

First element of 𝕩.

↗️
        1, 2, 3
 1
@@ -15,7 +15,7 @@
         a
 0
 
-

𝕨 𝕩: Pick

+

𝕨 𝕩: Pick

Pick the element of 𝕨 at index 𝕩.

↗️
       2  1, 2, 3
 3
-- 
cgit v1.2.3