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/depth.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'docs/help/depth.html') diff --git a/docs/help/depth.html b/docs/help/depth.html index 6412a932..5824fc71 100644 --- a/docs/help/depth.html +++ b/docs/help/depth.html @@ -5,7 +5,7 @@

Circle With Two Dots ()

-

𝔽𝕘 𝕩, 𝕨 𝔽𝕘 𝕩: Depth

+

𝔽𝕘 𝕩, 𝕨 𝔽𝕘 𝕩: Depth

Apply 𝔽 to the cells of the arguments at depth given in 𝕘.

↗️
       11 ⟨⟨1,2,3, 4,5,6⟩⟩
 ⟨ ⟨ 2 3 ⟩ ⟨ 5 6 ⟩ ⟩
-- 
cgit v1.2.3