| commit | 46a74d9726669469bba0e801c6b4fb5decb90d27 | [log] [tgz] |
|---|---|---|
| author | Gilles Peskine <Gilles.Peskine@arm.com> | Tue Dec 20 14:11:56 2022 +0100 |
| committer | Gilles Peskine <Gilles.Peskine@arm.com> | Thu Dec 22 10:36:36 2022 +0100 |
| tree | 0e05a40193078d7657ed60b3971e168443544ae4 | |
| parent | 5520d6a25df2227d420efc4bfbacb820314c2b5c [diff] |
Re-enable pr-head The lack of pr-head is a problem. We can't get any CI results if there's a merge conflict. Even with no conflict, pr-merge results change when the target branch changes, and we don't have an easy way to see if the pull request has had a passing job once pr-merge results become stale. So turn on pr-head. Explicitly mark the job as non-disabled by request. Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com> Change-Id: I5cb3679842f2857c212d2ccfa4a4be29ba58f9eb