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/repeat.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'docs/help/repeat.html') diff --git a/docs/help/repeat.html b/docs/help/repeat.html index 100bd413..67d8e002 100644 --- a/docs/help/repeat.html +++ b/docs/help/repeat.html @@ -5,7 +5,7 @@

Circle Star ()

-

𝔽𝔾 𝕩, 𝕨 𝔽𝔾 𝕩: Repeat

+

𝔽𝔾 𝕩, 𝕨 𝔽𝔾 𝕩: Repeat

Apply 𝔾 to 𝕨 and 𝕩 and apply 𝔽 to 𝕩 that may times. If 𝕨 is given, keep it as a constant left argument.

If 𝔾 returns an array, give 𝔽𝕩 for each element.

↗️
       1 + 4
-- 
cgit v1.2.3