3 months of waiting...

[Les De Ridder]

On Friday, 7 February 2020 at 20:00:16 UTC, berni44 wrote:
> [...]
>
> * Labels. I havn't found a way to add labels to my PR. I guess, 
> I just can't. Some of them would be helpful, especially WIP 
> (and auto-merge ;-) ). Maybe the bot could recognise +WIP and 
> -WIP and just add and remove this label.

GitHub introduced 'draft' PRs[1] for this last year. Sadly it's 
not
yet[2] possible to turn a normal PR (back) into a draft PR.

More generally however, I agree it would be useful to allow 
contributors
to set certain labels.

[1] 
https://github.blog/2019-02-14-introducing-draft-pull-requests/
[2] https://github.community/t5/-/-/td-p/19107