]> 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:15:55 +0000 (10:15 +0100)
* top/maint.mk (sc_indent): Don't use grep -q.
Suggested by Bruno Haible.

top/maint.mk

index c121e37a3dde742c6a1c031b5bf58374564b797c..2692a370d88ccfc369e85697adf24145dd224dad 100644 (file)
@@ -1644,7 +1644,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)";                            \