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

Acute Accent (ยด)

-

๐”ฝยด ๐•ฉ: Fold

+

๐”ฝยด ๐•ฉ: Fold

Fold over ๐•ฉ with ๐”ฝ from right to left i.e. Insert ๐”ฝ between the elements of ๐•ฉ.

๐•ฉ must be a simple list (1 = =๐•ฉ).

โ†—๏ธ
       +ยด 1โ€ฟ2โ€ฟ3
@@ -20,7 +20,7 @@
        1-2-3
 2
 
-

๐•จ ๐”ฝยด ๐•ฉ: Fold With initial

+

๐•จ ๐”ฝยด ๐•ฉ: Fold With initial

Monadic fold, but use ๐•จ as initial right argument.

โ†—๏ธ
       5 +ยด 1โ€ฟ2โ€ฟ3
 11
-- 
cgit v1.2.3