CI: avoid pipe in makefile, correctly report error in CI when tests fail#2621

Merged

mmetc merged 1 commit intomasterfrom ci-pipefail

Nov 28, 2023

+4-4

Commits on Nov 28, 2023

CI: avoid pipe in makefile, correctly report error in CI when tests fail
mmetc
committed