diff --git a/dune-workspace b/dune-workspace.bench similarity index 88% rename from dune-workspace rename to dune-workspace.bench index 6597fe3190121d7b95f03a62def5238881a7b743..8fb35dda755764fd18de3796a916298ea28ec082 100644 --- a/dune-workspace +++ b/dune-workspace.bench @@ -1,8 +1,8 @@ (lang dune 2.8) -(context default) (context (default (name bench) + (profile bench) (instrument_with landmarks) (env (_ (env-vars ("OCAML_LANDMARKS" "auto")))))