diff options
| author | Théo Zimmermann | 2018-10-01 13:28:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-10-01 13:28:02 +0200 |
| commit | eee287f0049d551c7b510522e4d0b2b5f10c5b89 (patch) | |
| tree | 7363763918562c7026c61a89eaedf0aed3e15ede /dev | |
| parent | e315f7b3e3e31eda27ef9f752d58aa85707f77bd (diff) | |
| parent | 0a01590462678d8374f11ddc60d68a569fa3df9c (diff) | |
Merge PR #8608: [default.nix] Add odoc to the documentation build-inputs
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions