[dune] Configuration tweak following upstream recommendations.

Dune upstream suggested that `dune-workspace` should be used for developer-specific recommendations, thus, core settings are better place in the root `dune` file.
rlepigre · Oct 5, 2018 · 36fc6f2 · 36fc6f2
1 parent 55f22b0
commit 36fc6f2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 8 deletions.
diff --git a/dune b/dune
@@ -0,0 +1,4 @@
+; Add project-wide flags here.
+(env
+ (dev     (flags :standard))
+ (release (flags :standard)))
diff --git a/dune-workspace b/dune-workspace