You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The extra CI jobs introduced in idris-lang#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.
0 commit comments