This (old) patch appears to have been applied. (although it predates the move to 
src/*!)

Thanks, closing the ticket.

Reply via email to