aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-11 17:47:06 +0200
committerThéo Zimmermann2018-10-11 17:47:06 +0200
commit3cc21c7fd91bc09774e0502e224f32c9f66fb61f (patch)
tree01870a0add8ac5b104f176255bfc58a469e2ff63 /dune
parent132343514c811e9791d8b5f31de5be8906fab66c (diff)
parent823f41dc9fa54efc7c55d3e1df8df7e5797837fb (diff)
Merge PR #8681: [dune] Fix and improve flags:
Diffstat (limited to 'dune')
-rw-r--r--dune13
1 files changed, 9 insertions, 4 deletions
diff --git a/dune b/dune
index 4e78a2fe3f..b4a5266125 100644
--- a/dune
+++ b/dune
@@ -1,10 +1,15 @@
; Default flags for all Coq libraries.
(env
(dev (flags :standard -rectypes -w -9-27-50+40+60))
- (release (flags :standard -rectypes))
- (ireport
- (flags :standard -rectypes -w -9-27-50+40+60)
- (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))
+ (release (flags :standard -rectypes)
+ (ocamlopt_flags -O3 -unbox-closures))
+ (ireport (flags :standard -rectypes -w -9-27-50+40+60)
+ (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report)))
+
+; The _ profile could help factoring the above, however it doesn't
+; seem to work like we'd expect/like:
+;
+; (_ (flags :standard -rectypes)))
; Rules for coq_dune
(rule