diff options
| author | Adrien Devresse <adrien.devresse@epfl.ch> | 2016-09-20 14:31:23 +0000 |
|---|---|---|
| committer | Adrien Devresse <adrien.devresse@epfl.ch> | 2016-09-20 14:34:43 +0000 |
| commit | 7ef053c6327441bc7306ff6ee12fde2a42301ab4 (patch) | |
| tree | 5b9ac53cf5148c6a55399b95cd5ff8c994b26c3c /Makefile.config.in | |
| parent | 0d38b4c7926890decbe2b03ed8f84584a5ce9b8a (diff) | |
Add a new option to disable documentation generation at configure time
Diffstat (limited to 'Makefile.config.in')
| -rw-r--r-- | Makefile.config.in | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 3e7847e36..2db7172b1 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -33,5 +33,6 @@ pkglibdir = $(libdir)/$(PACKAGE_NAME) prefix = @prefix@ storedir = @storedir@ sysconfdir = @sysconfdir@ +doc_generate = @doc_generate@ xmllint = @xmllint@ xsltproc = @xsltproc@ |