[check] Ensure that sed is GNU sed.

This is particularly important on MacOS, where the GNU toolchain is an
optional add-on, but the BSD sed would be used silently by default.

Author: tkoeppe

tools/check-source.sh

@@ -22,6 +22,9 @@ function fail() {
 }
 
 
+# We require GNU tools.
+sed --version | grep -Fqe "GNU sed" || { echo "sed is not GNU sed"; exit 1; }
+
 # Find non-ASCII (Unicode) characters in the source
 LC_ALL=C grep -ne '[^ -~	]' *.tex |
     fail 'non-ASCII character' || failed=1