diff options
Diffstat (limited to 'coccinelle/run-coccinelle.sh')
| -rwxr-xr-x | coccinelle/run-coccinelle.sh | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/coccinelle/run-coccinelle.sh b/coccinelle/run-coccinelle.sh index 1373b53c5..e982e3b0f 100755 --- a/coccinelle/run-coccinelle.sh +++ b/coccinelle/run-coccinelle.sh @@ -1,7 +1,6 @@ #!/bin/bash -e for SCRIPT in ${@-*.cocci} ; do - [ "$SCRIPT" = "empty-if.cocci" ] && continue echo "--x-- Processing $SCRIPT --x--" TMPFILE=`mktemp` spatch --sp-file $SCRIPT --dir $(pwd)/.. 2> "$TMPFILE" || cat "$TMPFILE" |