Subject: bug#11732: Follow-up to bug#11732

From: martin rudalics <[email-masked]>
Date: Thu, 28 Jun 2018 14:25:29 +0200

> All you need is patches I attached, "diff" or "diff2" (not both).

Thank you.  I will try them (but certainly not on Windows 10 which I
don't have).

martin