aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/plugin_base.dune
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-10-29 13:38:29 +0100
committerPierre-Marie Pédrot2018-10-29 13:38:29 +0100
commit35f715a005063a2c6195c574d019ba202bcdc27b (patch)
tree5dc3edf54bc0d3db9a6cbd95f6225b16f36ef3ae /plugins/ssr/plugin_base.dune
parentd838a67707812cb496f0f0f83f1ebe5a65280c86 (diff)
parentcd8b8974e2d62a3c3c4d7572921b5a83cbb8642c (diff)
Merge PR #8667: [RFC] Vendoring of Camlp5
Diffstat (limited to 'plugins/ssr/plugin_base.dune')
-rw-r--r--plugins/ssr/plugin_base.dune1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ssr/plugin_base.dune b/plugins/ssr/plugin_base.dune
index de9053f1a0..a13524bb52 100644
--- a/plugins/ssr/plugin_base.dune
+++ b/plugins/ssr/plugin_base.dune
@@ -3,4 +3,5 @@
(public_name coq.plugins.ssreflect)
(synopsis "Coq's ssreflect plugin")
(modules_without_implementation ssrast)
+ (flags :standard -open Gramlib)
(libraries coq.plugins.ssrmatching))