diff options
| author | Emilio Jesus Gallego Arias | 2018-09-19 02:50:29 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-12-13 15:40:38 +0100 |
| commit | ddb3fae72826c0da3ba449be4ebc72e44c1ace16 (patch) | |
| tree | 8f0f6cb37ef357537d39e0d5e285011fc218d69e /config | |
| parent | 228f0d929bb5098d58cd285fde42bb08d70c6ee8 (diff) | |
[dune] [doc] Support for building the reference manual with Dune.
This is a reduced version of #8503 as to provide a way to build the
reference manual with Dune.
Dune 1.6 supports (experimentally) directories as targets, thus we
introduce a rule that will call `sphinx` to build the manual.
This only provides build, however generation of `.install` rules is
not done, it will be hopefully addressed in #8503.
Note that we set `expire: 1 month` for all the artifacts we build with
Dune. IMHO this makes most sense as not to abuse Gitlab's hosting,
however of course we could consider a different deployment strategy if
wanted.
Diffstat (limited to 'config')
| -rw-r--r-- | config/dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/config/dune b/config/dune index cc993b97c9..c146e7df67 100644 --- a/config/dune +++ b/config/dune @@ -7,7 +7,7 @@ ; Dune doesn't use configure's output, but it is still necessary for ; some Coq files to work; will be fixed in the future. (rule - (targets coq_config.ml Makefile) + (targets coq_config.ml coq_config.py Makefile) (mode fallback) (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX)) (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no)))) |