[[ not valid in /bin/sh

[audetto]

I am using Ubuntu 23.04 which links /bin/sh (the shell used by make, see https://www.gnu.org/software/make/manual/html_node/Choosing-the-Shell.html) to dash which does not support [[.

The solution is to force make to use bash with SHELL = /bin/bash

If I send a PR, would you accept it? Better solution?

[sonninnos]

Sure, let's see it.

[audetto]

#499

EDIT: or, a bigger change is to drop [[ for a more standard [.

[sonninnos]

Ah, I thought I tried all possibilities, but apparently the thing works fine with just singles:

diff --git a/Makefile b/Makefile
index 8080489ba..61a5d2830 100644
--- a/Makefile
+++ b/Makefile
@@ -461,21 +461,21 @@ endif

 $(OBJDIR)/%.o: %.c
        @mkdir -p $(dir $@)
-       @if [[ $(SILENT) -ne 1 ]]; then\
+       @if [ $(SILENT) -ne 1 ]; then\
                $(if $@, $(shell echo echo CC $<),);\
        fi
        $(CC) $(CFLAGS) -c -o $@ $<

 $(OBJDIR)/%.o: %.cpp
        @mkdir -p $(dir $@)
-       @if [[ $(SILENT) -ne 1 ]]; then\
+       @if [ $(SILENT) -ne 1 ]; then\
                $(if $@, $(shell echo echo CXX $<),);\
        fi
        $(CXX) $(CXXFLAGS) -c -o $@ $<

 $(OBJDIR)/%.o: %.cc
        @mkdir -p $(dir $@)
-       @if [[ $(SILENT) -ne 1 ]]; then\
+       @if [ $(SILENT) -ne 1 ]; then\
                $(if $@, $(shell echo echo CXX $<),);\
        fi
        $(CXX) $(CXXFLAGS) -c -o $@ $<

So should we do this instead?

[audetto]

Yes, this is simpler.