10ff5d5507
This avoids the supposed issue that in case that 'make' fails, the whole 'jobs.build-and-check' stops, and 'Build logs' isn't executed, and thus there's no indication in the GitHub UI why 'make' failed. Using a shell pipeline is OK; the exit code of 'make' isn't lost, as per <https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#jobsjob_idstepsshell>, 'bash' is being run with '-o pipefail'. |
||
|---|---|---|
| .. | ||
| Remark.yml | ||
| bootstrap.yml | ||
| ccpp.yml | ||
| clang-format.yml | ||
| docker.yml | ||