diff options
Diffstat (limited to 'dune-workspace')
| -rw-r--r-- | dune-workspace | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dune-workspace b/dune-workspace index 1e3d1c8..2b855ff 100644 --- a/dune-workspace +++ b/dune-workspace @@ -2,4 +2,4 @@ (env (dev - (flags :standard -warn-error -27-32))) + (flags :standard -warn-error -3-27-32))) |