I've added few labels related to PR:
PR: needs more work (author's turn)
PR: waiting for Travis to finish
and then we can use them in a query.
Only contributors (i.e. people with repository write access) can set or
remove these labels. I.e. most authors can't remove "needs more work"
when they think they're done, and they can't set a "please review" label.
I am currently working on a WSGI script that extracts label-setting
commands from PRs, e.g. [+WIP] to add the WIP label and [-WIP] to remove it.
It's not done yet (and will take a while until it is), but I can set up
a GitHub project to share the code if anybody is interested in speeding
this up.
Those are all PRs that either can be merged or reviewed. If after the
review the author needs to do more work, just add the label "PR: needs
more work (author's turn)".
E.g. I'd be unable to add that label, just like anybody else who does
reviews but does not have write access.
--
You received this message because you are subscribed to the Google Groups
"sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sympy.
To view this discussion on the web visit
https://groups.google.com/d/msgid/sympy/55775922.3000005%40durchholz.org.
For more options, visit https://groups.google.com/d/optout.
