diff options
| author | Emilio Jesus Gallego Arias | 2020-03-13 16:37:28 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-13 16:37:28 -0400 |
| commit | 5189661a3cc165d8f6cb943c07eb9d644f339102 (patch) | |
| tree | 9fa78a7fc1b1c1b3ad5b3351a219095f28fcf83e /doc/tools/docgram/dune | |
| parent | 0d32ecd637b05214228912e80a3d56fda60735e9 (diff) | |
| parent | 6d690bf1ea5ad7fedf91865f52091daedb0cf43c (diff) | |
Merge PR #11797: Dune build rules for doc_grammar and fullGrammar.
Ack-by: ejgallego
Diffstat (limited to 'doc/tools/docgram/dune')
| -rw-r--r-- | doc/tools/docgram/dune | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/doc/tools/docgram/dune b/doc/tools/docgram/dune new file mode 100644 index 0000000000..3afa21f2cf --- /dev/null +++ b/doc/tools/docgram/dune @@ -0,0 +1,30 @@ +(executable + (name doc_grammar) + (libraries coq.clib coqpp)) + +(env (_ (binaries doc_grammar.exe))) + +(rule + (targets fullGrammar) + (deps + ; Main grammar + (glob_files %{project_root}/parsing/*.mlg) + (glob_files %{project_root}/toplevel/*.mlg) + (glob_files %{project_root}/vernac/*.mlg) + ; All plugins except SSReflect for now (mimicking what is done in Makefile.doc) + (glob_files %{project_root}/plugins/btauto/*.mlg) + (glob_files %{project_root}/plugins/cc/*.mlg) + (glob_files %{project_root}/plugins/derive/*.mlg) + (glob_files %{project_root}/plugins/extraction/*.mlg) + (glob_files %{project_root}/plugins/firstorder/*.mlg) + (glob_files %{project_root}/plugins/funind/*.mlg) + (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/rtauto/*.mlg) + (glob_files %{project_root}/plugins/setoid_ring/*.mlg) + (glob_files %{project_root}/plugins/syntax/*.mlg)) + (action + (chdir %{project_root} (run doc_grammar -short -no-warn %{deps}))) + (mode promote)) |