Gert,
Could you please propose your patch to the mutter developers directly?
https://gitlab.gnome.org/GNOME/mutter/merge_requests
Or if that's too much work, just start by reporting this bug to the mutter developers here:
https://gitlab.gnome.org/GNOME/mutter/issues
Gert,
Could you please propose your patch to the mutter developers directly?
https:/ /gitlab. gnome.org/ GNOME/mutter/ merge_requests
Or if that's too much work, just start by reporting this bug to the mutter developers here:
https:/ /gitlab. gnome.org/ GNOME/mutter/ issues