From 1daf8d6fed6b576f1082b2654ce4ad087a0a91b8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 19 Mar 2026 00:22:55 -0400 Subject: [PATCH] delete plugin --- src/cc/plugin/dune | 5 ----- 1 file changed, 5 deletions(-) delete mode 100644 src/cc/plugin/dune diff --git a/src/cc/plugin/dune b/src/cc/plugin/dune deleted file mode 100644 index 46f79cee..00000000 --- a/src/cc/plugin/dune +++ /dev/null @@ -1,5 +0,0 @@ -(library - (name Sidekick_cc_plugin) - (public_name sidekick.cc.plugin) - (libraries containers iter sidekick.sigs sidekick.cc sidekick.util) - (flags :standard -w +32 -open Sidekick_util))