doc/gendoc.py
changeset 19423 5046fede7684
parent 19322 ff1586a3adc5
child 19424 762e51ce3411
--- 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)