From 62b1ee6c1ee5d604696a253e1afccf59426da53c Mon Sep 17 00:00:00 2001
From: Jan Rochel <jrochel@besport.com>
Date: Wed, 22 Mar 2023 17:16:16 +0100
Subject: [PATCH] add headache config for default dune workspace file

---
 headers/headache_config.txt | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/headers/headache_config.txt b/headers/headache_config.txt
index 1b9796eb7a2..dc8775f3dfe 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:";;"
 
 ############
-- 
GitLab