diff -r d9e86d656017 -r 5046fede7684 doc/gendoc.py --- a/doc/gendoc.py Tue Jul 16 01:29:14 2013 +0200 +++ b/doc/gendoc.py Wed Jul 03 21:49:37 2013 +0900 @@ -63,7 +63,7 @@ return d -def show_doc(ui): +def showdoc(ui): # print options ui.write(minirst.section(_("Options"))) for optstr, desc in get_opts(globalopts): @@ -157,4 +157,4 @@ return extensions.enabled().keys() + extensions.disabled().keys() if __name__ == "__main__": - show_doc(sys.stdout) + showdoc(sys.stdout)