bd6cbaf3b6
This situation can happen if stdout is redirected and back. stdout's FILE* has now changed, and the prompt and stdout end up on different buffers, meaning that stdout is not flushed before the next prompt.