diff options
| author | Emilio Jesus Gallego Arias | 2020-05-07 12:35:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 12:35:00 +0200 |
| commit | 18a78b53f6998d3af8f8bb1b7a6b5054af232d4e (patch) | |
| tree | 9de758c3074efee99d840ccfc7527e2b0d9cbe8e /tools | |
| parent | 325a644b3f5a5f8c1a86191004576e7c763ae9f3 (diff) | |
| parent | bd69c92a0224918b1d4116a73841a67e72bccd8a (diff) | |
Merge PR #12267: [ci] bump elpi to 1.11
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions