diff options
| author | Emilio Jesus Gallego Arias | 2018-06-17 12:52:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-17 12:52:54 +0200 |
| commit | 8854588be4e2e8249f6ad9d16a0fd0534d42b66d (patch) | |
| tree | bc546e5207844447596ab3d440f1c24c31855114 /dev/base_include | |
| parent | 955e5a63cd2405632bb535b81bbad2fbe74d0394 (diff) | |
| parent | 3af7a31a45d3b600a49fc0268fae03d793f121e7 (diff) | |
Merge PR #7844: Remove Elpi from Travis.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions