Closed Krastanov closed 1 month ago
All of this is copied from Graphs.jl. I did not put any link to docs. Should be straightforward to merge (especially if organization secrets for codecov are already set)
@gdalle I will merge these in a couple of days and do a few more maintenance/cleanup tasks unrelated to modifying the actual code (making sure tests run, having aqua and jet, etc). For each such task I will wait a couple of days in case someone wants to approach it differently, but I will not wait for a formal review given that it is not touching actual code. If that is against community guidelines I am happy to do it differently.
Why not merge it now and then do other PRs? In my experience, smaller PRs get merged faster.
I am the one that created the PR. I do not want to merge it immediately in case someone wants to dissent. But yes, indeed, other changes will be in separate PRs -- I did not mean to imply differently.
I noticed that we did not have branch protection enabled for the master branch so I did that now. From now on, all PR's require one approval before they can be merged.
Ah, noted! That is what I meant when I wrote "If that is against community guidelines I am happy to do it differently."
There was a minor typo that is now fixed. I will squash and merge.
copied from Graphs.jl