From 4a6e4795545104e07b4c3c307129b51951cc3557 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Fri, 6 Sep 2024 09:59:56 +0200 Subject: [PATCH] Remove [dune-workspace] file. --- dune-workspace | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 dune-workspace diff --git a/dune-workspace b/dune-workspace deleted file mode 100644 index e69de29bb..000000000