extract_docs.awk (used to extract devtest.rst from devtest.sh, and
similiarly with other scripts that have docs auto-generated) does not
work in mawk, which is the default in precise.
gawk is already the default choice in Fedora 19, and seems to be the
default in later versions of Ubuntu. Haven't tested Debian.
Change-Id: I00cf5137d8e39c78a5d52b2cf094365a56deb353