diff --git a/doc/gendoc.py b/doc/gendoc.py old mode 100644 new mode 100755 --- a/doc/gendoc.py +++ b/doc/gendoc.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python """usage: %s DOC ... where DOC is the name of a document