I haven't heard back from anyone about https://github.com/rust-lang/rust/pull/53821 for more than a week. How do we proceed?
the compiler team didn't manage to get through its whole agenda at the last meeting... let me see
in terms of the issues you're having not being able to push to @Oli 's branch anymore, my personal appproach would be to close Oli's PR and open your own.
(and have the latter PR reference the former)
well I was mostly asking for a decision
'cause reopening will get us at the end of the queue, and IIRC oli's going to be back some time next week
Can always slap a p=1 on it
@RalfJ can you point at a comment that crystallizes the question being decided?
@nikomatsakis I just wrote one: https://github.com/rust-lang/rust/pull/53821#issuecomment-425993073
ah, right, I remember this now