diff options
| author | Luke Shumaker <lukeshu@lukeshu.com> | 2017-05-13 00:22:13 -0400 |
|---|---|---|
| committer | Luke Shumaker <lukeshu@lukeshu.com> | 2017-05-13 00:22:13 -0400 |
| commit | 71687834dba46b8a49eab18630dc6c335d53d219 (patch) | |
| tree | 694cc230c983ba187944794456c9321c566a5c2e | |
| parent | d64cebd3a4a6f59d72994a985549990c04e02a6f (diff) | |
fix dependency tracking for man pages
| -rw-r--r-- | tools/xml_helper.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/xml_helper.py b/tools/xml_helper.py index 862930e59c..db8d5ba2bb 100644 --- a/tools/xml_helper.py +++ b/tools/xml_helper.py @@ -50,6 +50,6 @@ def xml_parse(page): _deps.clear() doc = tree.parse(page, _parser) doc.xinclude() - return doc, _deps + return doc, _deps.copy() def xml_print(xml): return tree.tostring(xml, pretty_print=True, encoding='utf-8') |