diff options
| author | Gavin Thomas Claugus <gclaugus@gmail.com> | 2016-07-03 13:09:20 -0400 |
|---|---|---|
| committer | Gavin Thomas Claugus <gclaugus@gmail.com> | 2016-07-03 13:09:20 -0400 |
| commit | c0042196daf1679a1307009e709a7476fe55ab87 (patch) | |
| tree | 1e764fd13302f01695075f01941d80f4500c3372 /doc | |
| parent | 0185ab3fd8bc6df1e118d163f0f74b572bcfbc16 (diff) | |
Add DOCUMENT_SETTINGS_MAN variable
Signed-off-by: Gavin Thomas Claugus <gclaugus@gmail.com>
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/doc/Makefile b/doc/Makefile index 49e7da3e..af2916cc 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -53,6 +53,9 @@ DOCUMENT_SETTINGS_HTML= \ --table-of-contents \ --webtex +DOCUMENT_SETTINGS_MAN= \ + --variable section=5 \ + # # # |