Op zondag 19 februari 2017 11:45:06 CET schreef David Carlson: > *Bug 747333* <https://bugzilla.gnome.org/show_bug.cgi?id=747333> was > already filed some time ago, although that is just to document the current > behavior. > > David C > Indeed. And I even commented on that bug, yet had forgotten about it. Geert