diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5d76d407b4..b7067c8962 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -228,7 +228,9 @@ misc:sid:amd64: 🐞:sid:amd64: <<: *precheck_job - script: util/check-cocci + script: + - util/check-cocci + - if test "$(git status --porcelain | grep -Ev '\?\?' | wc -l)" -gt "0"; then git status --short; exit 1; fi # Jobs for doc builds on Debian Sid (amd64) diff --git a/util/check-cocci b/util/check-cocci index e6d501d7bf..48bd132773 100755 --- a/util/check-cocci +++ b/util/check-cocci @@ -1,10 +1,18 @@ #!/bin/sh -set -e +ret=0 for spatch in cocci/*.spatch; do + patch="$(dirname "$spatch")/$(basename "$spatch" .spatch).patch" + : > "$patch" for dir in bin lib fuzz; do - spatch --sp-file="$spatch" --use-gitgrep --dir "$dir" --in-place --quiet + spatch --sp-file="$spatch" --use-gitgrep --dir "$dir" --very-quiet --include-headers >> "$patch"; done + if [ "$(< "$patch" wc -l)" -gt "0" ]; then + cat "$patch" + ret=1 + else + rm "$patch" + fi done -exit 0 +exit $ret