diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-06 15:59:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-07 19:51:43 +0100 |
| commit | 90df0b3b217d4c588c236d1e56639320401f7aff (patch) | |
| tree | d7a9eeecebbb27cf71949568d872f483417e3eba /vernac/vernacentries.ml | |
| parent | 67a28c487fc64e2c0f8271b77d0c9db0cd82fa92 (diff) | |
gitlab: install num for all jobs
Previously it was installed for the compilation jobs causing random
failures when the other jobs got a cache without it.
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions