diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-08 09:21:19 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-08 09:27:27 -0700 |
| commit | 38951e35015ac373afcca23bc4ef8a38782f97cd (patch) | |
| tree | 43ff90aa78e673d87d931b9d18ec943c4c572365 /contrib/new-theory | |
| parent | d8994e79a67778b99e03dbe5a9437c4eb75c6c06 (diff) | |
Warn about trailing spaces in src/Makefile.am
The contrib/new-theory script expects no trailing whitespaces in
src/Makefile.am otherwise it inserts the list files of the new theory at
a wrong place in the file. This commit adds a check for that in the
beginning of the script. Since contrib/new-theory is run as part of our
Travis tests, this will allow us to detect trailing spaces and fix them
rather than silently ignoring them.
Diffstat (limited to 'contrib/new-theory')
| -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 |