]> Savannah Git Hosting - gnulib.git/commitdiff
maintainer-makefile: Fix last sc_indent commit.
authorSimon Josefsson <simon@josefsson.org>
Tue, 1 Nov 2022 08:09:02 +0000 (09:09 +0100)
committerBruno Haible <bruno@clisp.org>
Sun, 1 Jan 2023 09:46:53 +0000 (10:46 +0100)
* top/maint.mk (sc_indent): Don't use grep -q.
Suggested by Bruno Haible.

top/maint.mk

index 94babfd2eb624edfed04e0d22f5e257099314721..4844ac4da4ccd405ba4f64cdf07776894f2eeed2 100644 (file)
@@ -1653,7 +1653,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)";                            \