diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-28 16:33:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-28 16:33:41 +0200 |
| commit | a76730b8479b9036e814cc3ff5e7f32d46fc942c (patch) | |
| tree | 83f23277072f8cebe66fe7606f87eea85e5d3a1b /Makefile.doc | |
| parent | 75c144b25de008c85ff085761f80035a5a6278dd (diff) | |
| parent | 65b1c7a4f516ff1f60b39dd36c8ba967df18f84c (diff) | |
Merge PR #7376: Fix gitlab ubuntu version
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions