diff options
-rwxr-xr-x | configure.py | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/configure.py b/configure.py index 3de3c5815..b892389e3 100755 --- a/configure.py +++ b/configure.py @@ -2491,14 +2491,16 @@ class AmalgamationHeader(object): if name in self.included_already: return - if name == 'botan.h': - return - self.included_already.add(name) if name not in self.file_contents: return + depr_marker = 'BOTAN_DEPRECATED_HEADER(%s)\n' % (name) + if depr_marker in self.file_contents[name]: + logging.debug("Ignoring deprecated header %s", name) + return + for line in self.file_contents[name]: header = AmalgamationHelper.is_botan_include(line) if header: |