diff options
| author | Gaetan Gilbert | 2017-05-05 14:11:12 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-05-17 09:12:40 +0200 |
| commit | 8252ff7ef7159a2493dd5ac76a647a8b96a5a692 (patch) | |
| tree | 7854aa6287420275c4db1bae468f09bf24f1cd22 /Makefile.dev | |
| parent | f6b0d8b78ae25c8b1c6b901e57a5f4e38f20cdbd (diff) | |
Travis: deduplicate package list for coqide+documentation targets
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions