idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-08-16 08:40:37 +03:00
Code Issues Projects Releases Wiki Activity

[ ci ] re 3067: fix CI on main branch

Browse Source 
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.
This commit is contained in:
Thomas E. Hansen 2023-09-15 10:36:37 +02:00 committed by CodingCellist
parent 0029257eec
commit dc79c6dd05
1 changed files with 15 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
.github/workflows/ci-idris2-and-libs.yml vendored
View File

@ -627,7 +627,14 @@ jobs:
- name: Build idris2-pack
run: |
git config --global --add safe.directory "${PWD}"
git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
# only fetch to a new branch if we're not on main (otherwise, git complains)
if [[ $(git branch --show-current) != 'main' ]]
then git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
else git pull origin main
fi
# rebuild pack with the fetched Idris2
pack install pack
######################################################################
@ -663,7 +670,13 @@ jobs:
- name: Build pack with PR-Idris
run: |
git config --global --add safe.directory "${PWD}"
git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
# only fetch to a new branch if we're not on main (otherwise, git complains)
if [[ $(git branch --show-current) != 'main' ]]
then git fetch "https://github.com/${GITHUB_REPOSITORY}" "${GITHUB_REF}:${GITHUB_REF_NAME}"
else git pull origin main
fi
pack install pack
- name: Build+install idris2-lsp
run: |