projects / feed / packages.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fa631e9) | patch
CI: checkout HEAD commit rather than merge commit
authorPaul Spooren <mail@aparcar.org>
Fri, 5 Mar 2021 09:16:00 +0000 (23:16 -1000)
committerPaul Spooren <mail@aparcar.org>
Fri, 5 Mar 2021 09:42:32 +0000 (23:42 -1000)
commit13c1f2bcda33ab8fc17ede1f43f60e0aac8b7cab
treee57a5240557f6053c2a0a97a0fdc0cea7c2206c2tree | snapshot
parentfa631e92840dfc3fd13951dd56f54761e19ca3e7commit | diff
CI: checkout HEAD commit rather than merge commit

GitHub CI actions/checkout uses a merge commit which isn't compatible
with our formality checks. Instead checkout the pull request HEAD.

Signed-off-by: Paul Spooren <mail@aparcar.org>
.github/workflows/formal.yml diff | blob | history
Mirror of packages feed