Changeset 7a9d968 for doc/user-guide/genhelp.py

Timestamp:

2018-03-10T11:30:39Z (6 years ago)

Author:

Wilmer van der Gaast <wilmer@…>

Children:

5447c59

Parents:

3f44e43 (diff), 4a9c6b0 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge branch 'master' into HEAD

File:

• doc/user-guide/genhelp.py (modified) (1 diff)

doc/user-guide/genhelp.py

@@ -73 +73 @@
 
 def process_file(filename, parent=None):
-    tree = ET.parse(open(filename)).getroot()
+    try:
+        tree = ET.parse(open(filename)).getroot()
+    except:
+        sys.stderr.write("\nException while processing %s\n" % filename)
+        raise
     fix_tree(tree)
     return parse_tag(tree, parent)