doc/gendoc.py
changeset 45830 c102b704edb5
parent 44975 1a4b9b602e54
child 46516 921e1253c8ba
equal deleted inserted replaced
45829:e7a4c018b563 45830:c102b704edb5
     1 #!/usr/bin/env python
     1 #!/usr/bin/env python3
     2 """usage: %s DOC ...
     2 """usage: %s DOC ...
     3 
     3 
     4 where DOC is the name of a document
     4 where DOC is the name of a document
     5 """
     5 """
     6 
     6