doc/gendoc.py
changeset 45830 c102b704edb5
parent 44975 1a4b9b602e54
child 46516 921e1253c8ba
--- a/doc/gendoc.py	Mon Nov 09 09:58:44 2020 -0800
+++ b/doc/gendoc.py	Fri Nov 06 13:58:59 2020 -0800
@@ -1,4 +1,4 @@
-#!/usr/bin/env python
+#!/usr/bin/env python3
 """usage: %s DOC ...
 
 where DOC is the name of a document