Closed jfdm closed 3 years ago
Recently, idris2 switch the name of their default branch from master to main. This is a good idea.
master
main
I propose we do the same for idris-mode.
If there are no objections by the end of this week, I will make the change, and make a PR to melpa itself.
Done.
Recently, idris2 switch the name of their default branch from
master
tomain
. This is a good idea.I propose we do the same for idris-mode.
If there are no objections by the end of this week, I will make the change, and make a PR to melpa itself.