diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/dune | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/dune b/kernel/dune index 4f2e0e4e28..01abdb8f67 100644 --- a/kernel/dune +++ b/kernel/dune @@ -18,3 +18,4 @@ ; warnings. (env (dev (flags :standard -w +a-4-44-50))) + ; (ocaml408 (flags :standard -w +a-3-4-44-50))) |