aboutsummaryrefslogtreecommitdiff
path: root/dune
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-09-03 15:29:53 +0200
committerEmilio Jesus Gallego Arias2018-09-06 20:05:02 +0200
commit69e2490396c1f664350a957149d94ac9894d3c23 (patch)
treeb76441d5aa81dbe4c508ec0f498f368272b470fa /dune
parent51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff)
[dune] [ci] Fix and test release profile + use 1.1 dune-workspace
Dune 1.1 allows us to define the `env` flags in the workspace file, which is a better place than the current situation. Along the way, We fix the build flags for release mode [missing `-rectypes` and add a `release` build profile CI job.
Diffstat (limited to 'dune')
-rw-r--r--dune4
1 files changed, 0 insertions, 4 deletions
diff --git a/dune b/dune
index 2a77d62a16..b758fc7b56 100644
--- a/dune
+++ b/dune
@@ -9,7 +9,3 @@
(name vodeps)
(deps tools/coq_dune.exe .vfiles.d))
; (action (run coq_dune .vfiles.d))))
-
-; Add custom flags here. Default developer profile is `dev`
-(env
- (dev (flags :standard -rectypes -w -9-27-50)))