diff options
Diffstat (limited to 'doc/tools.texi')
| -rw-r--r-- | doc/tools.texi | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/tools.texi b/doc/tools.texi index 4427ffe56..d6e130f17 100644 --- a/doc/tools.texi +++ b/doc/tools.texi @@ -811,7 +811,7 @@ case a short name is not known. @item default This field is defined only for options for which the @code{default} or @code{default desc} flag is set. If the @code{default} flag is set, -its format is that of an @emph{option argument} (@xref{Format +its format is that of an @emph{option argument} (@pxref{Format conventions}, for details). If the default value is empty, then no default is known. Otherwise, the value specifies the default value for this option. If the @code{default desc} flag is set, the field is @@ -821,7 +821,7 @@ not given. @item argdef This field is defined only for options for which the @code{optional arg} flag is set. If the @code{no arg desc} flag is not set, its -format is that of an @emph{option argument} (@xref{Format +format is that of an @emph{option argument} (@pxref{Format conventions}, for details). If the default value is empty, then no default is known. Otherwise, the value specifies the default argument for this option. If the @code{no arg desc} flag is set, the field is |