diff --git a/dev-support/ci/xml_to_md.py b/dev-support/ci/xml_to_md.py index e07def6e02e..2afe3c096b4 100644 --- a/dev-support/ci/xml_to_md.py +++ b/dev-support/ci/xml_to_md.py @@ -27,6 +27,7 @@ Property = namedtuple('Property', ['name', 'value', 'tag', 'description']) + def extract_xml_from_jar(jar_path, xml_filename): xml_files = [] with zipfile.ZipFile(jar_path, 'r') as jar: