diff options
| author | Emilio Jesus Gallego Arias | 2017-02-07 15:58:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-07 17:33:57 +0100 |
| commit | fedf877e14ed75fd7156a97f5bd6dcdc9c6ffcef (patch) | |
| tree | ab329661c977fcd2369f27bfdc9d47a5d0027ec3 /plugins/extraction | |
| parent | 2a59cdce8c142d451988709a3939b884c63993c9 (diff) | |
[travis] [External CI] [geocoq] don't build slow file
Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15
minutes which is too much for Travis. Pity, because it was a nice use case.
Diffstat (limited to 'plugins/extraction')
0 files changed, 0 insertions, 0 deletions