Edward Chow c2df98c49c CI: Add workaround for github uppercase usernames ... The workflow defined in tools.yml and kernel.yml used to fail on forked repositories of contributers whose github username contains uppercase letters. A workaround mentioned in https://github.com/orgs/community/discussions/27086 and https://stackoverflow.com/questions/70326569/ is applied. Signed-off-by: Edward Chow <equu@openmail.cc> (cherry picked from commit c27b439564)		2022-12-04 17:36:56 +01:00
..
scripts	ci: show build failures directly in job log output	2022-12-04 17:36:55 +01:00
Dockerfile.tools	CI: create Docker container containing compiled tools	2022-12-04 17:36:55 +01:00
formal.yml	ci: move scripts into separate directory	2022-12-04 17:36:54 +01:00
kernel.yml	CI: Add workaround for github uppercase usernames	2022-12-04 17:36:56 +01:00
labeler.yml	CI: labeler: fix wrong label for pr targeting stable branch	2022-12-01 01:57:01 +01:00
tools.yml	CI: Add workaround for github uppercase usernames	2022-12-04 17:36:56 +01:00