diff options
| author | MarcoFalke <*~=`'#}+{/-|&$^_@721217.xyz> | 2023-07-19 11:22:12 +0200 |
|---|---|---|
| committer | MarcoFalke <*~=`'#}+{/-|&$^_@721217.xyz> | 2023-07-19 11:39:50 +0200 |
| commit | ffff4b5dc57c32bf759b705530c1368de4aa787e (patch) | |
| tree | f063f9c8ccdfe7e2caeb50f9672cb77eb6ca117d /ci/lint | |
| parent | fadc5232f49ebe0e23599cf76d6aadbd63e575b9 (diff) | |
lint: Add missing `set -ex` to ci/lint/06_script.sh
This is needed for the container-entrypoint.sh
Also, remove unused `source` from ci/lint_run_all.sh, since it is the
last step.
Diffstat (limited to 'ci/lint')
| -rwxr-xr-x | ci/lint/06_script.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ci/lint/06_script.sh b/ci/lint/06_script.sh index fa28f6126c..ccde12a033 100755 --- a/ci/lint/06_script.sh +++ b/ci/lint/06_script.sh @@ -6,6 +6,8 @@ export LC_ALL=C +set -ex + if [ -n "$LOCAL_BRANCH" ]; then # To faithfully recreate CI linting locally, specify all commits on the current # branch. |