Parcourir la source

Ignore files not ending with '.xml' when building doc header

mhilbrunner il y a 7 ans
Parent
commit
487afde3bb
1 fichiers modifiés avec 2 ajouts et 0 suppressions
  1. 2 0
      editor/SCsub

+ 2 - 0
editor/SCsub

@@ -39,6 +39,8 @@ def make_doc_header(target, source, env):
     docend = ""
     for s in source:
         src = s.srcnode().abspath
+        if not src.endswith(".xml"):
+            continue
         f = open_utf8(src, "r")
         content = f.read()
         buf+=content