diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:25:38 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:25:38 +0100 |
| commit | 2f9a5ba5b952ab2c660bf465aae71f383198804c (patch) | |
| tree | 93b25a6bf173590fc8d1b12b04a5ed0e707dc0ce /vernac/vernacentries.ml | |
| parent | 374d1efc5de20f8c99c13a7216357a7228c353e8 (diff) | |
| parent | 90df0b3b217d4c588c236d1e56639320401f7aff (diff) | |
Merge PR #6928: gitlab: install num for all 4.06 jobs
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions