diff options
| author | Glenn Morris <rgm@gnu.org> | 2018-02-21 20:44:37 -0500 |
|---|---|---|
| committer | Glenn Morris <rgm@gnu.org> | 2018-02-21 20:44:37 -0500 |
| commit | 56161254838e759243ccaab50c80327316a99979 (patch) | |
| tree | 09f336f86ecd9791629927e3e6cd2102a6887835 /admin/automerge | |
| parent | d48e07aaed0baf81baf377a9f2745678c9a5d41b (diff) | |
| download | emacs-56161254838e759243ccaab50c80327316a99979.tar.gz | |
* admin/automerge: Speed up check phase.
Diffstat (limited to 'admin/automerge')
| -rwxr-xr-x | admin/automerge | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/admin/automerge b/admin/automerge index 18f8c759ebc..76c1596f3fa 100755 --- a/admin/automerge +++ b/admin/automerge @@ -213,7 +213,8 @@ echo "Build finished ok" echo "Testing..." -make "$@" check || die "check error" +## We just want a fast pass/fail, we don't want to debug. +make "$@" check TEST_LOAD_EL=no || die "check error" echo "Tests finished ok" |