| commit | 963493ae7f82b77ac340e6b9bec051565f74b83b | [log] [tgz] |
|---|---|---|
| author | Gilles Peskine <Gilles.Peskine@arm.com> | Tue Dec 20 14:11:56 2022 +0100 |
| committer | Gilles Peskine <Gilles.Peskine@arm.com> | Tue Dec 20 15:28:51 2022 +0100 |
| tree | 73495deaffa8128c3d1c36aa96735ba6035ae4df | |
| parent | 0b3c469c2dfe863741e63bc117f4f1e6b3b52b30 [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. Signed-off-by: Gilles Peskine <Gilles.Peskine@arm.com> Change-Id: I5cb3679842f2857c212d2ccfa4a4be29ba58f9eb