diff options
| author | Emilio Jesus Gallego Arias | 2020-01-17 01:25:06 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-01-17 18:02:33 +0100 |
| commit | a47e2f6587e3507a12d4d86b9769b93e01023350 (patch) | |
| tree | 495c3402489dfcfeb78d903a0e5011cf75017b37 /Makefile.doc | |
| parent | 55ded80878d47037e49ca9b60f89c422d184899f (diff) | |
[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]
This partially fixes #10139 ; we now build the Ltac2 documentation and
deploy it.
The fix here can be used for inspiration to do the make-based part.
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions