From 89e7fe210608dac602e87cef13460779b9545869 Mon Sep 17 00:00:00 2001 From: Steve Linton Date: Tue, 23 Jul 2019 12:00:49 +0100 Subject: [PATCH] Undocument unused second argument for `DeclareGlobalFunction` --- lib/oper.g | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/oper.g b/lib/oper.g index ebd7742fe3..f208f33b8f 100644 --- a/lib/oper.g +++ b/lib/oper.g @@ -1794,12 +1794,12 @@ end ); ############################################################################# ## -#F DeclareGlobalFunction( , ) . . create a new global function +#F DeclareGlobalFunction( ) . . . . . . create a new global function #F InstallGlobalFunction( , ) ## ## <#GAPDoc Label="DeclareGlobalFunction"> ## -## +## ## ## ##