From 820dbc075d197e392befb737948cbb9e82af22a1 Mon Sep 17 00:00:00 2001 From: Joris van der Hoeven Date: Fri, 20 Nov 2020 20:12:11 +0000 Subject: [PATCH] Cleaning --- devel/scheme/api/glue-auto-doc.en.tm | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/devel/scheme/api/glue-auto-doc.en.tm b/devel/scheme/api/glue-auto-doc.en.tm index 297d8b3..70f46ba 100644 --- a/devel/scheme/api/glue-auto-doc.en.tm +++ b/devel/scheme/api/glue-auto-doc.en.tm @@ -6267,7 +6267,15 @@ source code. <\explain> - tree )> + )> + + <|explain> + Calls the function which returns + . + + + <\explain> + tree )> <|explain> Calls the function which returns