From 32fb1656e7d98b77af43fd72889e9da9fa391a82 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 10 Oct 2018 20:25:15 +0200
Subject: [quote] Remove spurious file after deletion of quote plugin.

For some reason PR #7894 left this spurious file; this is typical of a
bad resolution of a merge, and while the file is innocuous it should
go away.
---
 plugins/quote/plugin_base.dune       | 5 -----
 plugins/setoid_ring/plugin_base.dune | 2 +-
 2 files changed, 1 insertion(+), 6 deletions(-)
 delete mode 100644 plugins/quote/plugin_base.dune

(limited to 'plugins')

diff --git a/plugins/quote/plugin_base.dune b/plugins/quote/plugin_base.dune
deleted file mode 100644
index 323906acb2..0000000000
--- a/plugins/quote/plugin_base.dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name quote_plugin)
- (public_name coq.plugins.quote)
- (synopsis "Coq's quote plugin")
- (libraries coq.plugins.ltac))
diff --git a/plugins/setoid_ring/plugin_base.dune b/plugins/setoid_ring/plugin_base.dune
index 101246e28f..d83857edad 100644
--- a/plugins/setoid_ring/plugin_base.dune
+++ b/plugins/setoid_ring/plugin_base.dune
@@ -2,4 +2,4 @@
  (name newring_plugin)
  (public_name coq.plugins.setoid_ring)
  (synopsis "Coq's setoid ring plugin")
- (libraries coq.plugins.quote))
+ (libraries coq.plugins.ltac))
-- 
cgit v1.2.3