From 4f2da48207010b5edca8f0a9a4c5afe7e10eec17 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 27 Apr 2019 15:37:09 +0200
Subject: [meta] [dune] Fix discrepancies in plugin names

We have some discrepancy with the package names for plugins in the
META / Dune case. This PR fixes it.

At some point there was a need for plugin package names having to be
named as their directories.

I think this is not true anymore, but taking the "dir_name ==
package_name" convention just in case.
---
 plugins/funind/plugin_base.dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/plugin_base.dune')

diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune
index 002eb28eea..6ccf15df29 100644
--- a/plugins/funind/plugin_base.dune
+++ b/plugins/funind/plugin_base.dune
@@ -1,5 +1,5 @@
 (library
  (name recdef_plugin)
- (public_name coq.plugins.recdef)
+ (public_name coq.plugins.funind)
  (synopsis "Coq's functional induction plugin")
  (libraries coq.plugins.extraction))
-- 
cgit v1.2.3