| commit | 979ef3595f38705daedb47d7de276b37a2e822c1 | [log] [tgz] |
|---|---|---|
| author | Antonio García-Domínguez <agarcdomi@gmail.com> | Thu Jun 04 16:55:31 2020 +0100 |
| committer | Antonio García-Domínguez <agarcdomi@gmail.com> | Thu Jun 04 16:55:34 2020 +0100 |
| tree | 6b112f0d13048be8ec2cd4ed6f3b21938047ef6e | |
| parent | 4d10e3e8f1813ab8e36d98e3ccb5731715723d56 [diff] |
Core Jenkinsfile: allow for manual rebuilds
