From d3a51ac24244f586dfeff1a93b68cb084370534e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 11 Jan 2021 14:47:13 -0800
Subject: Remove the omega tactic and related options

---
 doc/tools/docgram/dune | 1 -
 1 file changed, 1 deletion(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune
index 4ba60ddd9f..873b2f8dff 100644
--- a/doc/tools/docgram/dune
+++ b/doc/tools/docgram/dune
@@ -21,7 +21,6 @@
    (glob_files %{project_root}/plugins/ltac/*.mlg)
    (glob_files %{project_root}/plugins/micromega/*.mlg)
    (glob_files %{project_root}/plugins/nsatz/*.mlg)
-   (glob_files %{project_root}/plugins/omega/*.mlg)
    (glob_files %{project_root}/plugins/ring/*.mlg)
    (glob_files %{project_root}/plugins/rtauto/*.mlg)
    (glob_files %{project_root}/plugins/ssr/*.mlg)
-- 
cgit v1.2.3