diff options
| author | Emilio Jesus Gallego Arias | 2019-02-18 19:36:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-18 19:36:27 +0100 |
| commit | fcc3ee5d3eed4703e88fc1a2f07006130b61d006 (patch) | |
| tree | 3f9fd5a85025d4e12db7a0484206e353e6dd695e /Makefile.dev | |
| parent | ee6d8274483711f84277e449494c3a11a64dfea8 (diff) | |
| parent | 7e03019c888161cb027dd76c3fa393d3d8f442e5 (diff) | |
Merge PR #9597: [ci] Resolve commit corresponding to branch when downloading tarball.
Reviewed-by: SkySkimmer
Reviewed-by: ejgallego
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions