| commit | 46ba93c4eaf0ec81379916b0173b4bdc5ea60da2 | |
| author | Mikhail Glushenkov <mikhail.glushenkov@gmail.com> | |
| Sat, 12 Aug 2017 15:22:55 +0000 (12 16:22 +0100) | ||
| committer | Mikhail Glushenkov <mikhail.glushenkov@gmail.com> | |
| Sat, 12 Aug 2017 15:37:56 +0000 (12 16:37 +0100) | ||
| tree | 8bbc38220f3feac774bf0889800a17a644e7dd0d | treesnapshot (tar.gz zip) |
| parent | 65830e96b72745d867ae4df8afc3e7d6874124b8 | commitdiff |
Makefile: generate the user guide with Sphinx.
Fixes #4622.
[ci skip]
(cherry picked from commit ef2078d7f831210b6bfb0606bea7b670008a9271)
Fixes #4622.
[ci skip]
(cherry picked from commit ef2078d7f831210b6bfb0606bea7b670008a9271)
| Cabal/Makefile | diffblobblamehistory |