GitHub allows better collaboration on forks and PRs

[Denis Davydov]

FYI, https://github.com/blog/2247-improving-collaboration-with-forks

Essentially, if contributor cliks a checkbox, maintainers will be able to push changes to contributors branches in PRs.

Cheers,

Denis.

[David Wells]

This looks useful, but I think we should avoid using it frequently. We should try to get contributors to fix their own things.

[Denis Davydov]

Agree.

--
You received this message because you are subscribed to a topic in the Google Groups "deal.II developers" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/dealii-developers/IPna_RNvFOY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to dealii-develop...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.