mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-19 09:12:34 +03:00
dc79c6dd05
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. |
||
---|---|---|
.. | ||
ISSUE_TEMPLATE | ||
linters | ||
scripts | ||
workflows | ||
pull_request_template.md |