On Fri, Apr 27, 2018 at 03:24:35PM +0200, Geert Janssens wrote: > It think it's worth reporting as a bug, though of low priority. Done: https://bugzilla.gnome.org/show_bug.cgi?id=795613 Thanks, - Eric