diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-10 11:50:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-10 11:50:43 +0200 |
| commit | 45171b6e34f01392dabee285f616f3f6f4217e98 (patch) | |
| tree | 17f7ab4c276678b608477e35709088fba0c6379f /Makefile.doc | |
| parent | 372737ba74baa2af8ee798df1b2768a5d827a179 (diff) | |
| parent | 42c6b8f3b13cc5e974a129fe81481e64c9a8a182 (diff) | |
Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1.
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions