In September Github has rolled out a few new features, one of the is
>From the interface it appears to be more handy than simply tagging
One can prioretize issues/PRs and shift things around. Essentially it's a
way to organize Issues and PRs for a better visualization and
Here is a video: https://www.youtube.com/watch?v=C6MGKHkNtxU
I think this could be used for: (i) upcoming release (ii) starter projects
(iii) big milestones like full complex-valued support.
p.s. one can also gather all comments on a PR into a single review and do
one of the following: ask for changes / approve / just comment. I like this
feature as well.
You received this message because you are subscribed to the Google Groups
"deal.II developers" group.
To unsubscribe from this group and stop receiving emails from it, send an email
For more options, visit https://groups.google.com/d/optout.