From 67718bb448fecc4f86420ce633964bd267f2c2b9 Mon Sep 17 00:00:00 2001
From: ·𐑑𐑴𐑕𐑑𐑩𐑤
Date: Sat, 20 Dec 2025 18:56:53 +0000
Subject: Dune-related EditorConfig stuff

---
 .editorconfig | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to '.editorconfig')

diff --git a/.editorconfig b/.editorconfig
index 83152ee..d7cd0de 100644
--- a/.editorconfig
+++ b/.editorconfig
@@ -20,6 +20,19 @@ indent_size = unset
 indent_style = space
 indent_size = 3
 
-[dune,dune-project,dune-workspace]
+[dune]
 indent_style = space
 indent_size = 1
+
+[dune-project]
+indent_style = space
+indent_size = 1
+
+[dune-workspace]
+indent_style = space
+indent_size = 1
+
+# Dune is generating Opam files so I have no control. Should I skip Dune here?
+[*.opam]
+indent_style = unset
+indent_size = unset
-- 
cgit v1.2.3