From 7b29a128c40b60d6dc743106fc04b514d3cde7ae Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
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