Idris2

idris-lang/Idris2

Fork 0

mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-20 10:02:03 +03:00

Commit Graph

Author	SHA1	Message	Date
CodingCellist	46be3b8082	[ ci ] Update deploy-action in ci-idris2-and-libs.yml (#3115 )	2023-10-23 15:26:20 +01:00
Thomas E. Hansen	dc79c6dd05	[ ci ] re 3067: fix CI on main branch The extra CI jobs introduced in #3067 work fine as long as 'main' is not the checked out branch. This is due to the fetch to a new branch, which git does (reasonably) not allow when you're trying to fetch 'main' into a new branch that's also called 'main'. In this case, we should just `git pull origin main`, which is what the script now (hopefully) does.	2023-09-15 12:05:10 +02:00
CodingCellist	9d083154a5	Test pack and lsp during CI (#3067 )	2023-09-13 17:37:49 +01:00

Author

SHA1

Message

Date

CodingCellist

46be3b8082

[ ci ] Update deploy-action in ci-idris2-and-libs.yml (#3115 )

2023-10-23 15:26:20 +01:00

Thomas E. Hansen

dc79c6dd05

[ ci ] re 3067: fix CI on main branch

The extra CI jobs introduced in #3067 work fine as long as 'main' is not
the checked out branch. This is due to the fetch to a new branch, which
git does (reasonably) not allow when you're trying to fetch 'main' into
a new branch that's also called 'main'. In this case, we should just
`git pull origin main`, which is what the script now (hopefully) does.

2023-09-15 12:05:10 +02:00

CodingCellist

9d083154a5

Test pack and lsp during CI (#3067 )

2023-09-13 17:37:49 +01:00

3 Commits