JB> Mixing fprintf and stderr shouldn't be done lightly as the output won't be ordered with that of cerr. I think we're better to still use cerr unless we're in a bad alloc situation.

WS> I have explained this change in the ticket. Do you agree with my explanation?