diff options
Diffstat (limited to 'doc/dune')
| -rw-r--r-- | doc/dune | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/doc/dune b/doc/dune new file mode 100644 index 0000000000..54ffa87205 --- /dev/null +++ b/doc/dune @@ -0,0 +1,24 @@ +(rule + (targets sphinx_build) + (deps + ; We could use finer dependencies here so the build is faster: + ; + ; - vo files: generated by sphinx after parsing the doc, promoted, + ; - Static files: + ; + %{bin:coqdoc} etc... + ; + config/coq_config.py + ; + tools/coqdoc/coqdoc.css + (package coq) + (source_tree sphinx) + (source_tree tools)) + (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + +(alias + (name refman-html) + (deps sphinx_build)) + +; The install target still needs more work. +; (install +; (section doc) +; (package coq-refman) +; (files sphinx_build)) |
