diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-09 11:10:42 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-09 11:11:29 +0100 |
| commit | 8f56790546e74cadf62d91c7078853bcced11e37 (patch) | |
| tree | f2b746ffb81c92735bf96fe213993de1c9b371c1 /dev/include | |
| parent | d9f79d97dbc503e149cba2df1b228a94d7ac970b (diff) | |
Fix ci-bignums.sh "missing ]" error.
It made the test always fail so ci-common was always sourced. It's not
quite idempotent as it adds COQBIN to PATH but it didn't lead to CI failure.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions