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/export.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'docs/help/export.html') diff --git a/docs/help/export.html b/docs/help/export.html index 6fee8a1c..5fbbef78 100644 --- a/docs/help/export.html +++ b/docs/help/export.html @@ -13,7 +13,7 @@ ns.unexported Error: No key found -

𝕨 ⇐: Export names

+

𝕨 ⇐: Export names

Export the names given in 𝕩 from the current namespace or program's scope. Names must be defined.

↗️
    ns1 ← { ⟨alsoexported⟩⇐, exported ⇐ 5, alsoexported ← 0}
     ns1.exported
-- 
cgit v1.2.3