Document the import REPL escape.

(cherry picked from commit 65782f775195b5ab383183a323e2423072303c1e)

diff --git a/doc/user-manual/user.texinfo b/doc/user-manual/user.texinfo
index 313b736e2530a26e47a1aec70caf52d46229e7ae..5763c06051fd8872179733a1039297413c5b65b1 100644 (file)
--- a/doc/user-manual/user.texinfo
+++ b/doc/user-manual/user.texinfo
@@ -1504,6 +1504,11 @@ Creates a new child @acronym{REPL} with the same current environment
 as this one.
 @end deffn
 
+@deffn {REPL command} import import-set @dots{}
+Imports the given @var{import-set}s into the current @acronym{REPL}
+environment.  The syntax is described in @rseven{} section 5.2.
+@end deffn
+
 @deffn {REPL command} up
 Pops up one level to the parent @acronym{REPL}.