diff options
| author | jvoisin | 2023-08-20 21:33:33 +0200 |
|---|---|---|
| committer | jvoisin | 2023-08-20 21:33:33 +0200 |
| commit | 737b5207e12bb12a270fa1a385048fcf55617e43 (patch) | |
| tree | dc4255486d1a673d0d556d9721da9601ea449501 /include | |
| parent | bfbaa577f6fc46ebb965724e0f261e79e26ec9fb (diff) | |
Specify "shell: bash" in github actions
As [documented](https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#exit-codes-and-error-action-preference),
this brings us `set -eo pipefail`.
Diffstat (limited to 'include')
0 files changed, 0 insertions, 0 deletions