From deb584c0e17aa0bd67cdd40fc63cc3d6611d9574 Mon Sep 17 00:00:00 2001
From: Victor Zverovich <victor.zverovich@gmail.com>
Date: Fri, 12 Jan 2024 13:56:00 -0800
Subject: [PATCH] Update build.py

---
 doc/build.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/build.py b/doc/build.py
index 743f3ec6..8d70886e 100755
--- a/doc/build.py
+++ b/doc/build.py
@@ -54,7 +54,7 @@ def build_docs(version='dev', **kwargs):
       GENERATE_MAN      = NO
       GENERATE_RTF      = NO
       CASE_SENSE_NAMES  = NO
-      INPUT             = {0}/args.h {0}/core.h {0}/chrono.h {0}/color.h \
+      INPUT             = {0}/args.h {0}/base.h {0}/chrono.h {0}/color.h \
                           {0}/compile.h {0}/format.h {0}/os.h {0}/ostream.h \
                           {0}/printf.h {0}/ranges.h {0}/xchar.h
       QUIET             = YES