On Mon, Jan 18, 2016 at 05:46:00PM -0500, Leo Famulari wrote: > Shall we open a bug for this? It was discussed in #22013 [0] but that > specific issue was solved and the bug was closed in expectation of a > more general bug report.
I think it would be helpful to not forget the problem. Andreas
