diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 21:39:05 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:40 -0400 |
| commit | 17be4f1e005b233e75c37acad3aadba45fd780dd (patch) | |
| tree | fabaf4d5662147f373fc58acfd344e1ee3a174f7 | |
| parent | 875d0f0b01339aab4e60c408f1d7aa601e9653e6 (diff) | |
Minor Doxygen fixes.
| -rw-r--r-- | config/doxygen.cfg | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/config/doxygen.cfg b/config/doxygen.cfg index c92610873..f05485542 100644 --- a/config/doxygen.cfg +++ b/config/doxygen.cfg @@ -570,9 +570,11 @@ WARN_LOGFILE = INPUT = $(SRCDIR)/AUTHORS \ $(SRCDIR)/COPYING \ + $(SRCDIR)/INSTALL \ $(SRCDIR)/NEWS \ $(SRCDIR)/README \ - $(SRCDIR)/ChangeLog \ + $(SRCDIR)/RELEASE-NOTES \ + $(SRCDIR)/THANKS \ $(CVC4_DOXYGEN_INPUT) # This tag can be used to specify the character encoding of the source files |