GUDHI/gudhi-devel

`master` default branch should be renamed `main`

VincentRouvreau opened this issue 8 months ago · 1 comments

VincentRouvreau commented 8 months ago

cf. https://www.git-tower.com/learn/git/faq/git-rename-master-to-main/ for a how-to