documentation: it's Doxyfile.xml I shall ignore, not Doxyfile.html.

Made an error in 45911a18 and apparently it was fine because it silently
returned in some later check.

diff --git a/documentation/doxygen.py b/documentation/doxygen.py
index 207975f265e628a9ea04b18cf307a4976baa7c58..3d34a01e1b2974bfbe1b18cd6c68a785529d9b1b 100755 (executable)
--- a/documentation/doxygen.py
+++ b/documentation/doxygen.py
@@ -2536,7 +2536,7 @@ def parse_xml(state: State, xml: str):
 
     # All these early returns were logged in extract_metadata() already, no
     # need to print the same warnings/errors twice. Keep the two consistent.
-    if state.current == 'Doxyfile.html':
+    if state.current == 'Doxyfile.xml':
         return
 
     logging.debug("Parsing {}".format(state.current))