diff options
Diffstat (limited to 'grammar/dune')
| -rw-r--r-- | grammar/dune | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/grammar/dune b/grammar/dune index 90847e7fb6..f03fe07607 100644 --- a/grammar/dune +++ b/grammar/dune @@ -18,6 +18,7 @@ (install (section bin) + (package coq) (files coqp5 coqmlp5)) (rule |