We have Work in progress and Experimental labels created before GitHub had "Draft PR" feature. Draft PR is nicer because it actually disables the merge button. Should we remove these labels in favor of using Draft PR exclusively?
Might also want to add bot logic to check if a PR is draft or not, so cc @astrofrog , @bsipocz , and @Cadair .
We have
Work in progressandExperimentallabels created before GitHub had "Draft PR" feature. Draft PR is nicer because it actually disables the merge button. Should we remove these labels in favor of using Draft PR exclusively?Might also want to add bot logic to check if a PR is draft or not, so cc @astrofrog , @bsipocz , and @Cadair .