Warn about trailing spaces in src/Makefile.am (#1759)

diff --git a/contrib/new-theory b/contrib/new-theory
index b349e78b01d5909139de757b9e5e60cb51a75988..9e4e92a71591409bf1451583c479ef09c8a64612 100755 (executable)
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -16,6 +16,13 @@ if [ ! -e src/theory/theory_engine.h ]; then
   exit 1
 fi
 
+# Trailing whitespaces in src/Makefile.am mess with the regexps (and are
+# generally undesirable, so we throw an error instead of ignoring them).
+if grep -q '[[:blank:]]$' src/Makefile.am; then
+       echo "ERROR: trailing whitespaces in src/Makefile.am" >&2
+       exit 1
+fi
+
 if [ $# -ge 1 -a "$1" = --alternate ]; then
   shift
   alternate=true