diff options
author | 2018-04-28 16:33:41 +0200 | |
---|---|---|
committer | 2018-04-28 16:33:41 +0200 | |
commit | a76730b8479b9036e814cc3ff5e7f32d46fc942c (patch) | |
tree | 83f23277072f8cebe66fe7606f87eea85e5d3a1b /vernac/vernacentries.ml | |
parent | 75c144b25de008c85ff085761f80035a5a6278dd (diff) | |
parent | 65b1c7a4f516ff1f60b39dd36c8ba967df18f84c (diff) |
Merge PR #7376: Fix gitlab ubuntu version
Diffstat (limited to 'vernac/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions