diff --git a/util/check-cocci b/util/check-cocci index d9268b808d..7231596c9d 100755 --- a/util/check-cocci +++ b/util/check-cocci @@ -3,7 +3,10 @@ ret=0 for spatch in cocci/*.spatch; do patch="$(dirname "$spatch")/$(basename "$spatch" .spatch).patch" - spatch --sp-file="$spatch" --use-gitgrep --dir bin --dir lib --dir fuzz --very-quiet > "$patch"; + : > "$patch" + for dir in bin lib fuzz; do + spatch --sp-file="$spatch" --use-gitgrep --dir "$dir" --very-quiet >> "$patch"; + done if [ "$(< "$patch" wc -l)" -gt "0" ]; then cat "$patch" ret=1