I confirm the bug. can't we wait for the next update of editline instead this the patch was merged and conditions to trigger are quite specific (if you open the repl in a wide terminal and narrow it afterwards, the bug is not triggered).

I confirm the bug. can't we wait for the next update of editline instead this the patch was merged and conditions to trigger are quite specific

Oh, hooray I somehow missed it being merged. :3. We can wait if that sounds better 👍.

(if you open the repl in a wide terminal and narrow it afterwards, the bug is not triggered).

I don't believe this is entirely true-- I think you need to hit enter or something before the new size is respected? Anyway it's not likely something many folks encounter, which I think is the point :).

I don't believe this is entirely true-- I think you need to hit enter or something before the new size is respected? Anyway it's not likely something many folks encounter, which I think is the point :).

Exactly :D so feel free to merge but I don't think it's worth the trouble.

Do we know what's the ETA on an upstream release with the patch? Couple days, few weeks probably this can be left for an upstream update. Longer may be annoying.

In any ways, if the update is a breaking one, the patch might need to be backported to 19.03, as a QOL patch.

Gonna propose we merge in a week or two (2019-05-15) if we don't have an ETA by then, and otherwise re-evaluate. But upstream seems to be fairly responsive, so I suspect we'll hit the latter case.

Merging this, as promised.