diff options
| author | Emilio Jesus Gallego Arias | 2019-05-28 19:11:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-28 19:11:02 +0200 |
| commit | 09514118c386420650847ba74c7f985bb0a05776 (patch) | |
| tree | 584840db738c643a903655126e26a7586c7a8487 /doc/plugin_tutorial/Makefile | |
| parent | 13eeeb7d36e5d8ed669e856ecf69baf83c6eb330 (diff) | |
| parent | cee21dc9caa8890d2fc77eb10da47902b4e3eacf (diff) | |
Merge PR #10228: gitlab: run less jobs unless FULL_CI=true
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions