Automate MIP number selection
Closed this issue · 1 comments
BelfordZ commented
We should make a gh action that, on PR merge to main, renames any file in mips/mip-x.md to the next number and pushes it up.
New mips should be submitted with this file naming scheme, and we should update docs to reflect this.
This way, any new mip automatically gets assigned a number when it is approved & merged
shanejonas commented
this was fixed in #6