diff --git a/.cocciconfig b/.cocciconfig index 43967c6b2015..5d734a503031 100644 --- a/.cocciconfig +++ b/.cocciconfig @@ -1,3 +1,3 @@ -[spatch] +[spatch]: options = --timeout 200 options = --use-gitgrep