diff options
Diffstat (limited to 'java/makedist.py')
| -rwxr-xr-x | java/makedist.py | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/java/makedist.py b/java/makedist.py index 7d99fbe0b34..91a40a2fe34 100755 --- a/java/makedist.py +++ b/java/makedist.py @@ -18,7 +18,7 @@ def usage(): print print "Options:" print "-h Show this message." - print "-d Skip SGML documentation conversion." + print "-d Skip documentation conversion." print "-t Skip building translators and use the ones in PATH." print "-f Keep going if precondition checks fail." print "-v Be verbose." @@ -329,7 +329,8 @@ version = re.search("ICE_STRING_VERSION = \"([0-9\.b]*)\"", config.read()).group print "Fixing version in README and INSTALL files..." fixVersion(find("icej", "README*"), version) fixVersion(find("icej", "INSTALL*"), version) -fixVersion(find("icej/doc", "index.html"), version) +if not skipDocs: + fixVersion(find("icej/doc", "index.html"), version) # # Create source archives. |