diff options
| -rwxr-xr-x | web-export/update.py | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/web-export/update.py b/web-export/update.py index cd54f28..8f3a3ef 100755 --- a/web-export/update.py +++ b/web-export/update.py @@ -133,7 +133,7 @@ class SpecObject(): self.filename = '%s-%s%s' % (self.basename_no_ext, self.version, self.ext) - if self.ext not in ['.xml', '.sgml', '.txt', '.dtd']: + if self.ext not in ['.xml', '.sgml', '.txt', '.dtd', '.html']: raise Exception('Format \'%s\' not supported for %s' % (self.ext, self.vcs.get_url())) self.downloaded = False @@ -161,6 +161,9 @@ class SpecObject(): if not self.downloaded and not force: return + if self.ext == '.html': + return + path = os.path.join(self.spec_dir, self.filename) (path_no_ext, ext) = os.path.splitext(path) |