From a96ee5044238934e2a44a5cf37a74b6aaeb6413c Mon Sep 17 00:00:00 2001
From: Carlo Wood <carlo@alinoe.com>
Date: Sun, 6 Nov 2016 02:17:30 +0100
Subject: [PATCH] Stop people from using broken awk.

---
 Tools/fix_headers.sh | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/Tools/fix_headers.sh b/Tools/fix_headers.sh
index c08d3c432b..390153ef65 100755
--- a/Tools/fix_headers.sh
+++ b/Tools/fix_headers.sh
@@ -8,6 +8,16 @@ function fatal
 	exit 1
 }
 
+# Make sure we're not having a broken gawk.
+AWK_VERSION=$(awk -V | head -n 1)
+if [[ $AWK_VERSION =~ ^GNU\ Awk\ 4\.[0-9]+\.[0-9]+ ]]; then
+	AWK_VERSION=$(echo $AWK_VERSION | sed -e 's/GNU Awk \(4\.[0-9]*\.[0-9]*\).*/\1/')
+	if [[ $AWK_VERSION =~ ^4\.0*([2-9]+|1\.0*[2-9]+) ]]; then
+		fatal "Your version of awk ($AWK_VERSION) is broken. Please use version 4.1.1 or lower."
+	fi
+fi
+echo "AWK_VERSION=$AWK_VERSION"
+
 # Find out what the base directory is.
 BASEDIR="$(dirname $(dirname $(readlink -en "$0")))"
 echo "BASEDIR=\"$BASEDIR\""
@@ -864,7 +874,7 @@ function fixup_header
 	fi
 }
 
-if [ $debug -ne 0 ]; then
+if [ $non_option_arguments -ne 0 ]; then
 	fixup_header $1
 	exit
 fi