diff --git a/testing/external/Makefile b/testing/external/Makefile index 25efdad05b..502451dcee 100644 --- a/testing/external/Makefile +++ b/testing/external/Makefile @@ -6,11 +6,11 @@ DIAG=diag.log all: @rm -f $(DIAG) - @for repo in $(REPOS); do (cd $$repo && make -s ); done + @for repo in $(REPOS); do ( cd $$repo && make -s ); done brief: @rm -f $(DIAG) - @for repo in $(REPOS); do (cd $$repo && make -s brief ); done + @for repo in $(REPOS); do ( cd $$repo && make -s brief ); done init: git clone $(PUBLIC_REPO) @@ -25,9 +25,9 @@ status: @for repo in $(REPOS); do ( cd $$repo && echo '>>' $$repo && git status -bs && echo ); done coverage: - @for repo in $(REPOS); do (cd $$repo && echo "Coverage for '$$repo' repo:" && make coverage); done + @for repo in $(REPOS); do ( cd $$repo && echo "Coverage for '$$repo' repo:" && make coverage ); done update-timing: - @for repo in $(REPOS); do (cd $$repo && echo "Coverage for '$$repo' repo:" && make update-timing); done + @for repo in $(REPOS); do ( cd $$repo && echo "Updating timing for '$$repo' repo:" && make update-timing ); done .PHONY: all brief init pull push status coverage