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 682631e7dc..aae70e598b 100644 --- a/dune-workspace +++ b/dune-workspace @@ -1,4 +1,4 @@ -(lang dune 1.1) +(lang dune 1.2) ; Add custom flags here. Default developer profile is `dev` (env |