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/enlist_pair.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'docs/help/enlist_pair.html') diff --git a/docs/help/enlist_pair.html b/docs/help/enlist_pair.html index a1470004..2915532b 100644 --- a/docs/help/enlist_pair.html +++ b/docs/help/enlist_pair.html @@ -5,7 +5,7 @@

Bow Tie ()

-

𝕩: Enlist

+

𝕩: Enlist

Put 𝕩 in a single element list. (𝕩)

↗️
       1
 ⟨ 1 ⟩
@@ -20,7 +20,7 @@
              ┘  
                ┘
 
-

𝕨 𝕩: Pair

+

𝕨 𝕩: Pair

Put 𝕨 and 𝕩 in a two element list. (𝕨, 𝕩)

↗️
      1  2
 ⟨ 1 2 ⟩
-- 
cgit v1.2.3