diff options
Diffstat (limited to '.editorconfig')
| -rw-r--r-- | .editorconfig | 15 |
1 files changed, 14 insertions, 1 deletions
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 |