Meta/Dothem: support --cocci

diff --git a/Dothem b/Dothem
index 3a55a187250f7d5aa0436f9c33d904120968f202..84b620c67162d2bd6b31cbf26c7052ba428ec331 100755 (executable)
--- a/Dothem
+++ b/Dothem
@@ -18,11 +18,13 @@ inst_prefix=$(
 )
 
 force= with_dash= test_long= M= install= nodoc= notest= bootstrap= branches= jobs=
-scratch= noprove= memtrash=--memtrash
+scratch= noprove= memtrash=--memtrash with_cocci=
 while  case "$1" in
        --pedantic | --locale=* | --loose) M="$M $1" ;;
        --force) force=$1 ;;
        --dash) with_dash=y ;;
+       --cocci) with_cocci=y ;;
+       --no-cocci) with_cocci= ;;
        --long) test_long=--long ;;
        --noinstall) install=noinstall ;;
        --nodoc) nodoc=y ;;
@@ -200,6 +202,11 @@ do
 
                save=$(git rev-parse HEAD) &&
 
+               if test -n "$with_cocci"
+               then
+                       Meta/Make $M $jobs -- coccicheck
+               fi &&
+
                Meta/Make $M $jobs -- SPARSE_FLAGS=-Wsparse-error sparse &&
 
                Meta/Make $M $noprove ${test+"$test"} $jobs $test_long $memtrash \