diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-08 16:50:40 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-08 18:50:40 -0500 |
| commit | e2816e7db1da33b3b4cee613e9bb67b0e1c16037 (patch) | |
| tree | ddce430f9f2cacff9854223e724fd44e976b0a1f /contrib | |
| parent | 245b73861187696d86bb7a6a6fdb281de89c26e4 (diff) | |
Warn about trailing spaces in src/Makefile.am (#1759)
Diffstat (limited to 'contrib')
| -rwxr-xr-x | contrib/new-theory | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/contrib/new-theory b/contrib/new-theory index b349e78b0..9e4e92a71 100755 --- 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 |