From e7729134e37622aed49de60e158477c0ea3477d2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Thu, 2 Mar 2023 16:11:52 +0900
Subject: [PATCH] move files from plugins directory as it seems to be used by
new plugin system by Dune (that's weird)
---
src/{plugins/mpfr => }/lustrec_mpfr.ml | 0
src/{plugins/mpfr => }/lustrec_mpfr.mli | 0
src/{plugins => }/pluginList.ml | 0
src/{plugins => }/pluginList.mli | 0
src/{plugins => }/pluginType.ml | 0
src/{plugins => }/pluginType.mli | 0
src/{plugins => }/plugins.ml | 0
src/{plugins => }/plugins.mli | 0
8 files changed, 0 insertions(+), 0 deletions(-)
rename src/{plugins/mpfr => }/lustrec_mpfr.ml (100%)
rename src/{plugins/mpfr => }/lustrec_mpfr.mli (100%)
rename src/{plugins => }/pluginList.ml (100%)
rename src/{plugins => }/pluginList.mli (100%)
rename src/{plugins => }/pluginType.ml (100%)
rename src/{plugins => }/pluginType.mli (100%)
rename src/{plugins => }/plugins.ml (100%)
rename src/{plugins => }/plugins.mli (100%)
diff --git a/src/plugins/mpfr/lustrec_mpfr.ml b/src/lustrec_mpfr.ml
similarity index 100%
rename from src/plugins/mpfr/lustrec_mpfr.ml
rename to src/lustrec_mpfr.ml
diff --git a/src/plugins/mpfr/lustrec_mpfr.mli b/src/lustrec_mpfr.mli
similarity index 100%
rename from src/plugins/mpfr/lustrec_mpfr.mli
rename to src/lustrec_mpfr.mli
diff --git a/src/plugins/pluginList.ml b/src/pluginList.ml
similarity index 100%
rename from src/plugins/pluginList.ml
rename to src/pluginList.ml
diff --git a/src/plugins/pluginList.mli b/src/pluginList.mli
similarity index 100%
rename from src/plugins/pluginList.mli
rename to src/pluginList.mli
diff --git a/src/plugins/pluginType.ml b/src/pluginType.ml
similarity index 100%
rename from src/plugins/pluginType.ml
rename to src/pluginType.ml
diff --git a/src/plugins/pluginType.mli b/src/pluginType.mli
similarity index 100%
rename from src/plugins/pluginType.mli
rename to src/pluginType.mli
diff --git a/src/plugins/plugins.ml b/src/plugins.ml
similarity index 100%
rename from src/plugins/plugins.ml
rename to src/plugins.ml
diff --git a/src/plugins/plugins.mli b/src/plugins.mli
similarity index 100%
rename from src/plugins/plugins.mli
rename to src/plugins.mli
--
GitLab