Ticket moved from /p/jedit/bugs/3213/