diff options
| author | R. Bernstein <rocky@gnu.org> | 2012-10-27 11:39:56 -0400 |
|---|---|---|
| committer | R. Bernstein <rocky@gnu.org> | 2012-10-27 11:39:56 -0400 |
| commit | 21f5a34ae55d2d175fec21b6dd42686f1078896e (patch) | |
| tree | 0bc6ca12b39849f0deade4ebfd5ac67e12fb3e30 | |
| parent | 8992c19eb93e5e732ed32a565de31a9b5f61a091 (diff) | |
make-check-short.rb: ignore gmake as you would make or remake
| -rwxr-xr-x | make-check-filter.rb | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/make-check-filter.rb b/make-check-filter.rb index 704f8bd6..535a240d 100755 --- a/make-check-filter.rb +++ b/make-check-filter.rb @@ -6,8 +6,8 @@ pats = '(' + ["^ CC", "^ CXX", - '^(re)?make\[', - "^(re)?make ", + '^(re|g)?make\[', + "^(re|g)?make ", "Making check in", '^[+]{2} WARN: ', '^m4/', # doesn't work always |