diff options
| author | Maxime Dénès | 2018-09-26 14:55:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-26 14:55:29 +0200 |
| commit | 5ced288419aed8a622ed2c267e35d9a174facafc (patch) | |
| tree | 2b4f617546ff718e2acad62d35fd7cf3f6d6467a /kernel/dune | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
| parent | 2cceef0e3cab18b1dcc28bf1c8ce6b4723cd3d9a (diff) | |
Merge PR #7571: [kernel] Compile with almost all warnings enabled.
Diffstat (limited to 'kernel/dune')
| -rw-r--r-- | kernel/dune | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/dune b/kernel/dune index 011af9c28c..a503238907 100644 --- a/kernel/dune +++ b/kernel/dune @@ -13,3 +13,8 @@ (documentation (package coq)) + +; In dev profile, we check the kernel against a more strict set of +; warnings. +(env + (dev (flags :standard -w +a-4-44-50))) |