diff options
| author | Simon Josefsson <simon@josefsson.org> | 2022-11-01 09:09:02 +0100 |
|---|---|---|
| committer | Simon Josefsson <simon@josefsson.org> | 2022-11-01 09:10:20 +0100 |
| commit | 757160ccb0fb5d86d09e415eb52ffa9a3a85be5b (patch) | |
| tree | 4ed95915d492ddfbbaa6548e7e3bac6aaf08b628 /top | |
| parent | 4555e788613f1f5d1e8519427591bef3274d3124 (diff) | |
| download | gnulib-757160ccb0fb5d86d09e415eb52ffa9a3a85be5b.tar.gz | |
maintainer-makefile: Fix last sc_indent commit.
* top/maint.mk (sc_indent): Don't use grep -q.
Suggested by Bruno Haible.
Diffstat (limited to 'top')
| -rw-r--r-- | top/maint.mk | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/top/maint.mk b/top/maint.mk index 85b15fb2d2..0b42438b2c 100644 --- a/top/maint.mk +++ b/top/maint.mk @@ -1663,7 +1663,7 @@ indent: # Running indent once is not idempotent, but running it twice is. indent $(indent_args) $(INDENT_SOURCES) sc_indent: - @if ! indent --version 2> /dev/null | grep -q 'GNU indent'; then\ + @if ! indent --version 2> /dev/null | grep 'GNU indent' > /dev/null; then \ echo 1>&2 '$(ME): sc_indent: GNU indent is missing'; \ else \ fail=0; files="$(INDENT_SOURCES)"; \ |