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