diff options
| author | Théo Zimmermann | 2020-04-24 14:39:22 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-24 17:03:00 +0200 |
| commit | 172c1c825061d450609468dd9c53974bfdb7d0cd (patch) | |
| tree | aa0c65da7e178e1c9bcda0fc95bb5529887b2a4d /doc/dune | |
| parent | 8c47247779b6db4c529510a7ce771162f54f5fbf (diff) | |
[dune] Fix dependencies of refman.
Dependencies specified through an alias do not trigger a rebuild when
they are modified. This is likely a Dune bug, but we still need to
fix this on our side as this is inconvenient.
Diffstat (limited to 'doc/dune')
| -rw-r--r-- | doc/dune | 18 |
1 files changed, 16 insertions, 2 deletions
@@ -23,7 +23,14 @@ (targets refman-html) (alias refman-html) (package coq-doc) - (deps (alias refman-deps)) + ; Cannot use this deps alias because of ocaml/dune#3415 + ; (deps (alias refman-deps)) + (deps + (package coq) + (source_tree sphinx) + (source_tree tools/coqrst) + unreleased.rst + (env_var SPHINXWARNOPT)) (action (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b html sphinx %{targets}))) @@ -31,7 +38,14 @@ (targets refman-pdf) (alias refman-pdf) (package coq-doc) - (deps (alias refman-deps)) + ; Cannot use this deps alias because of ocaml/dune#3415 + ; (deps (alias refman-deps)) + (deps + (package coq) + (source_tree sphinx) + (source_tree tools/coqrst) + unreleased.rst + (env_var SPHINXWARNOPT)) (action (progn (run env COQLIB=%{project_root} sphinx-build %{env:SPHINXWARNOPT=-W} -b latex sphinx %{targets}) |
