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 -----
 1 file changed, 5 deletions(-)
 delete mode 100644 plugins/quote/plugin_base.dune

(limited to 'plugins/quote')

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))
-- 
cgit v1.2.3