diff --git a/doc/build.py b/doc/build.py index 31049716..7133c7b5 100755 --- a/doc/build.py +++ b/doc/build.py @@ -74,7 +74,7 @@ def build_docs(version='dev', **kwargs): GENERATE_MAN = NO GENERATE_RTF = NO CASE_SENSE_NAMES = NO - INPUT = {0}/core.h {0}/format.h {0}/ostream.h \ + INPUT = {0}/core.h {0}/format.h {0}/os.h {0}/ostream.h \ {0}/printf.h {0}/time.h QUIET = YES JAVADOC_AUTOBRIEF = YES