diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-10 18:34:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-10 18:34:44 +0200 |
| commit | b4572185522cd21e7e4e1cf59095ae66d0da0be1 (patch) | |
| tree | 37803edada0dcd5b8c543c322c1839801b9e254d /plugins/ltac/tacinterp.mli | |
| parent | da13cd2f7bf29be080922dcf07f1fc6a9d4cb4ec (diff) | |
| parent | 6964772d33a7ee10c28b6f07767c0e391b7dd123 (diff) | |
Merge PR #8036: [travis] Remove even more jobs.
Diffstat (limited to 'plugins/ltac/tacinterp.mli')
0 files changed, 0 insertions, 0 deletions