| 06:31 | <ljharb> | sure, want me to do it next chance i get? i can do it in 12-14 hours or so |
| 20:08 | <bakkot> | ljharb: sure, please do |
| 20:09 | <bakkot> | I'm also happy to take care of it as long as the process is literally just clicking the rename button on the branches page on github, but if you want to do more than that I will leave it to you |
| 20:21 | <ljharb> | oh hmm |
| 20:22 | <ljharb> | yeah there's a tiny bit of extra cleanup |
| 20:22 | <ljharb> | but "Will close 1 open pull request for this branch." |
| 20:22 | <ljharb> | iow, that means one PR is probably something that we can't update, so i guess that's fine if it's closed |
| 20:24 | <ljharb> | k, everything should be updated |
| 20:29 | <bakkot> | I just got a bunch of notifications about apparently nonexistent PRs being closed |
| 20:29 | <bakkot> | I wonder if those were spam PRs that github created a number for but hid? |
| 20:30 | <bakkot> | they all seem to be gibberish |
| 20:31 | <bakkot> | like, 1508 - afaik there just isn't an issue or PR with that number, so presumably github hid it? |
| 20:32 | <bakkot> | except for https://github.com/tc39/ecma262/pull/1986, that was a real PR which got closed, presumably by accident? |