Minutes August 25 2020 - math-comp/math-comp GitHub Wiki
About the PR that were postponed for 1.11: Cyril will ping the authors, and they can put them back in the topics
About #357:
not ready for merge
author did not reply last ping
inserting a new structure may lead to performance problem
we close it saying that:
it can't be integrated as it is
we are working on the hierarchy, so maybe it will, but not soon
we believe it is interesting and should be published as a separate package
About #501, postponed to next meeting
About coqbot: Cyril did set a git attribute on CHANGELOG_UNRELEASED to use the merge=union strategy. When you rebase a PR atop master, and master contains new items in the changelog, you should not see any conflict (your changelog item is added). warning if you don't just add an item to the changelog, but rather touch other lines (eg fix a typo), the merge=union strategy does not work well.
About adding stuff to the MC organization, everybody is welcome.
A good name for mczify... if the plan is to merge it we can live with this not so nice name for a while.