diff options
Diffstat (limited to 'config')
| -rw-r--r-- | config/doxygen.cfg | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/config/doxygen.cfg b/config/doxygen.cfg index 78014290d..71d434959 100644 --- a/config/doxygen.cfg +++ b/config/doxygen.cfg @@ -568,8 +568,7 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = $(SRCDIR)/src \ - src +INPUT = $(CVC4_DOXYGEN_INPUT) # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is |