doc: fix PushOptions manual entry

gap-system · Nov 20, 2020 · f83ece9 · f83ece9
1 parent aac58b4
commit f83ece9
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/lib/options.gd b/lib/options.gd
@@ -57,11 +57,11 @@
 
 #############################################################################
 ##
-#F  PushOptions( <options record> )                           set new options
+#F  PushOptions( <options_record> )                           set new options
 ##
 ##  <#GAPDoc Label="PushOptions">
 ##  <ManSection>
-##  <Func Name="PushOptions" Arg='options record'/>
+##  <Func Name="PushOptions" Arg='options_record'/>
 ##
 ##  <Description>
 ##  This function pushes a record of options onto the global option stack.

diff --git a/lib/options.gi b/lib/options.gi
@@ -26,7 +26,7 @@ MakeReadOnlyGlobal("OptionsStack");
 
 #############################################################################
 ##
-#F  PushOptions( <options record> )                           set new options
+#F  PushOptions( <options_record> )                           set new options
 ##
 ##  This is a function, not an operation, so we need to check our arguments
 ##