From c7eecf1b10da6adb3518877808ff188b634061c2 Mon Sep 17 00:00:00 2001 From: imsahil007 <35963992+imsahil007@users.noreply.github.com> Date: Wed, 9 Oct 2019 18:09:03 +0530 Subject: [PATCH] Added colon --- .cocciconfig | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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