From a1f10626bed1db14ce116e9201ed05dadfc366b4 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 11 Sep 2018 14:32:22 +0200
Subject: Remove romega

---
 plugins/romega/plugin_base.dune | 5 -----
 1 file changed, 5 deletions(-)
 delete mode 100644 plugins/romega/plugin_base.dune

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

diff --git a/plugins/romega/plugin_base.dune b/plugins/romega/plugin_base.dune
deleted file mode 100644
index 49b0e10edf..0000000000
--- a/plugins/romega/plugin_base.dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name romega_plugin)
- (public_name coq.plugins.romega)
- (synopsis "Coq's romega plugin")
- (libraries coq.plugins.omega))
-- 
cgit v1.2.3