diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-20 11:10:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-20 11:10:57 +0200 |
| commit | 2ad49dc7a9c6ae327dc8b56491232a24c7bd347b (patch) | |
| tree | c6a17289db72d142ebb6054154aa17b562ac2c61 /library/lib.mli | |
| parent | d70a662da07aeeab9dc11544200864e402c0a9b5 (diff) | |
| parent | f8c0dbb29d260f9be0f188358d8d53145976a177 (diff) | |
Merge PR #5972: Fixing link to GitHub issue search, and wording.
Diffstat (limited to 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions