From 5d06c6be4bea0f3b3d31d9f35a29f9a7460679a4 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Sun, 15 May 2022 22:05:00 -0400 Subject: =?UTF-8?q?Add=20help=20sections=20for=20modified=20assignment=20F?= =?UTF-8?q?=E2=86=A9?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/help/export.html | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'docs/help/export.html') diff --git a/docs/help/export.html b/docs/help/export.html index 0dcf8dd7..a693a7a6 100644 --- a/docs/help/export.html +++ b/docs/help/export.html @@ -14,9 +14,9 @@ ns.unexported Error: No key found -

𝕨 ⇐: Export names

+

n ⇐: Export names

→full documentation

-

Export the names given in 𝕩 from the current namespace. Names must be defined somewhere in the scope.

+

Export the names given in n from the current namespace. Names must be defined somewhere in the scope.

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