diff options
Diffstat (limited to 'doc/cvc4.1_template.in')
| -rw-r--r-- | doc/cvc4.1_template.in | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in index ddf9bac09..a0535553b 100644 --- a/doc/cvc4.1_template.in +++ b/doc/cvc4.1_template.in @@ -48,9 +48,9 @@ is connected to a terminal, interactive mode is assumed. .IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option." -${common_manpage_documentation} +${man_common}$ -${remaining_manpage_documentation} +${man_others}$ .IP "Each option marked with [*] has a \-\-no\-OPTIONNAME variant, which reverses the sense of the option." |