projects / feed / packages.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 29ad225) | 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)
committerJosef Schlehofer <pepe.schlehofer@gmail.com>
Sun, 21 Aug 2022 21:33:12 +0000 (23:33 +0200)
commitf50a80b79cb97bf40267ad53fb43c304feefd36b
treeed7b25d759324781faba3b433254d88b920b4170tree | snapshot
parent29ad225700915998cad973d9919009c925d15944commit | 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>
(cherry picked from commit 13c1f2bcda33ab8fc17ede1f43f60e0aac8b7cab)
.github/workflows/formal.yml diff | blob | history
Mirror of packages feed