From ca678c3675a7aa1bd5b396b15660b7ab1163c193 Mon Sep 17 00:00:00 2001 From: Dan Liew <daniel.liew@imperial.ac.uk> Date: Mon, 24 Apr 2017 15:45:57 +0100 Subject: [PATCH] [Doxygen] Fix bug where `def_Type` directives in `z3.h` would appear in generated doxygen documentation. --- doc/mk_api_doc.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index bb5a19e5f..e86205a7a 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -50,15 +50,16 @@ def mk_dir(d): if not os.path.exists(d): os.makedirs(d) -# Eliminate def_API and extra_API directives from file 'inf'. +# Eliminate def_API, extra_API, and def_Type directives from file 'inf'. # The result is stored in 'outf'. def cleanup_API(inf, outf): pat1 = re.compile(".*def_API.*") pat2 = re.compile(".*extra_API.*") + pat3 = re.compile(r".*def_Type\(.*") _inf = open(inf, 'r') _outf = open(outf, 'w') for line in _inf: - if not pat1.match(line) and not pat2.match(line): + if not pat1.match(line) and not pat2.match(line) and not pat3.match(line): _outf.write(line) try: