diff options
author | Glenn Morris <rgm@gnu.org> | 2016-12-07 19:45:48 -0500 |
---|---|---|
committer | Glenn Morris <rgm@gnu.org> | 2016-12-07 19:45:48 -0500 |
commit | 5531e75385ca3d02287f4df7788e38090f70b6b7 (patch) | |
tree | cd91d6e990c85b3ab1103d9312db9ce6f794711c /make-dist | |
parent | 953bf67fbea6298cb68b7610fdc09c3fcdf8aeec (diff) | |
download | emacs-5531e75385ca3d02287f4df7788e38090f70b6b7.tar.gz |
Further improve make-dist checking
* make-dist: Print status messages when checking.
Diffstat (limited to 'make-dist')
-rwxr-xr-x | make-dist | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/make-dist b/make-dist index 31fa53a6f4d..e454e924480 100755 --- a/make-dist +++ b/make-dist @@ -204,6 +204,9 @@ them, and try again." >&2 fi if [ $check = yes ]; then + + echo "Sanity checking (use --no-check to disable this)..." + error=no ls -1 lisp/[a-zA-Z]*.el lisp/[a-z]*/[a-zA-Z0-9]*.el \ @@ -288,7 +291,11 @@ if [ $check = yes ]; then make --question info || error=yes fi - [ $error = yes ] && exit 1 + if [ $error = yes ]; then + echo "Failed checks" >&2 + exit 1 + fi + fi if [ $update = yes ]; then |