From 213d84a27bc0adeaa5ed56652b76c463070ff38e Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 10 Aug 2022 10:48:58 +0200
Subject: [PATCH] [build] bench workspace
---
dune-workspace => dune-workspace.bench | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
rename dune-workspace => dune-workspace.bench (88%)
diff --git a/dune-workspace b/dune-workspace.bench
similarity index 88%
rename from dune-workspace
rename to dune-workspace.bench
index 6597fe31901..8fb35dda755 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")))))
--
GitLab