diff options
| author | Théo Zimmermann | 2019-04-16 18:27:14 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-05 19:22:32 +0200 |
| commit | 30d6ffdd4546d56c517bef5b31a862c5454240f0 (patch) | |
| tree | 7fe923020598b54da28ad0043ef12481d1e300e8 /doc/dune | |
| parent | 6ff10c569c1684927d4cb866a159fe6f54e55abe (diff) | |
New infrastructure for the unreleased changelog.
Move existing entries.
Diffstat (limited to 'doc/dune')
| -rw-r--r-- | doc/dune | 6 |
1 files changed, 6 insertions, 0 deletions
@@ -11,6 +11,7 @@ (package coq) (source_tree sphinx) (source_tree tools) + unreleased.rst (env_var SPHINXWARNOPT)) (action (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) @@ -19,6 +20,11 @@ (name refman-html) (deps sphinx_build)) +(rule + (targets unreleased.rst) + (deps (source_tree changelog)) + (action (with-stdout-to %{targets} (bash "cat changelog/*.rst")))) + ; The install target still needs more work. ; (install ; (section doc) |
