diff --git a/src/check-doc-syntax.awk b/src/check-doc-syntax.awk
old mode 100755
new mode 100644
index 5fdabdac9..1fa8b8d22
--- a/src/check-doc-syntax.awk
+++ b/src/check-doc-syntax.awk
@@ -1,5 +1,3 @@
-#!/usr/bin/awk -f
-
 BEGIN {
     name_found = 1
     SECTION_DOC = 0
diff --git a/src/check-doc-syntax.sh b/src/check-doc-syntax.sh
index c74fb875d..762a48429 100755
--- a/src/check-doc-syntax.sh
+++ b/src/check-doc-syntax.sh
@@ -72,7 +72,7 @@ fi >&2
 
 # Only run the syntax checker on the source files (not doc/)
 if test -e ./check-doc-syntax.awk; then
-    if echo $FILES | xargs ./check-doc-syntax.awk ; then
+    if echo $FILES | xargs awk -f ./check-doc-syntax.awk ; then
 	    :
     else
 	    stat=1