diff options
| author | Théo Zimmermann | 2018-10-11 14:35:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-11 14:35:50 +0200 |
| commit | 4a6ddf4fdc4790fc407dc98bcfb80fd816cab304 (patch) | |
| tree | a28536dae55101f5643d7eb6ce1f64c71660afac /plugins | |
| parent | ea62cca89773e8101b7a81d15adbf15081eb5e0f (diff) | |
| parent | 32fb1656e7d98b77af43fd72889e9da9fa391a82 (diff) | |
Merge PR #8699: [quote] Remove spurious file after deletion of quote plugin.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/quote/plugin_base.dune | 5 | ||||
| -rw-r--r-- | plugins/setoid_ring/plugin_base.dune | 2 |
2 files changed, 1 insertions, 6 deletions
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)) |