Thanks a lot for this bug report. I also noticed this sometimes but was unable to reliably reproduce it.
I committed a change that should fix this. If anyone notices this behaviour again with a current checkout, feel free to reopen.
Thanks a lot for this bug report. I also noticed this sometimes but was unable to reliably reproduce it.
I committed a change that should fix this. If anyone notices this behaviour again with a current checkout, feel free to reopen.