diff --git a/headers/headache_config.txt b/headers/headache_config.txt index 1b9796eb7a29140f1deeb877ca7f8aef54a17006..dc8775f3dfebe242ecea234f667b4612af663b12 100644 --- a/headers/headache_config.txt +++ b/headers/headache_config.txt @@ -58,6 +58,8 @@ ######## | "dune-project" -> frame open:";;" line:";" close:";;" | ".*dune-project" -> skip match:"(lang.*" +| "dune-workspace" -> frame open:";;" line:";" close:";;" +| "dune-workspace" -> skip match:"(lang.*" | "dune" -> frame open:";;" line:";" close:";;" ############