From 6a11029aafffa902d2ec296a312da2387ec75f6d Mon Sep 17 00:00:00 2001 From: Joris van der Hoeven Date: Sun, 6 Dec 2020 18:30:36 +0000 Subject: [PATCH] Re-synchronize with comments editor when adding or suppressing comments --- devel/scheme/api/glue-auto-doc.en.tm | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/devel/scheme/api/glue-auto-doc.en.tm b/devel/scheme/api/glue-auto-doc.en.tm index 70f46ba..55f0433 100644 --- a/devel/scheme/api/glue-auto-doc.en.tm +++ b/devel/scheme/api/glue-auto-doc.en.tm @@ -8418,6 +8418,14 @@ source code. . + <\explain> + )> + + <|explain> + Calls the function which returns + . + + <\explain> )>