1 files changed, 3 insertions, 0 deletions
diff --git a/.cocciconfig b/.cocciconfig
new file mode 100644
index 000000000..43967c6b2
--- /dev/null
+++ b/.cocciconfig
@@ -0,0 +1,3 @@
+[spatch]
+	options = --timeout 200
+	options = --use-gitgrep