diff --git a/src/check-doc-syntax.sh b/src/check-doc-syntax.sh index e566a6ea8..bfda7a206 100755 --- a/src/check-doc-syntax.sh +++ b/src/check-doc-syntax.sh @@ -70,10 +70,13 @@ if echo $FILES | xargs grep "$note_regexp" /dev/null; then echo Be civil and replace it by 'Note' please. fi >&2 -if echo $FILES | xargs ./check-doc-syntax.awk ; then - : -else - stat=1 -fi >&2 +# Only run the syntax checker on the source files (not doc/) +if -e ./check-doc-syntax.awk; then + if echo $FILES | xargs ./check-doc-syntax.awk ; then + : + else + stat=1 + fi >&2 +fi exit $stat