No, in that case no report is needed.
Thanks for investigating!
Giovanni
On May 14, 2013 8:20 AM, "Bazon Bloch" <bazonbloch arcor de> wrote:
Am 13.05.2013 21:55, schrieb Giovanni Campagna:
maybe conflicts with otherthanks for that hint, indeed it is!
extensions claiming "gnome-shell-extensions" gettext domain)
after many supends and resumes I found out: https://extensions.gnome.org/extension/355/status-area-horizontal-spacing/ causes this. i have left a bug report there.
Really file a bug for Gnome-Shell anyway?
regards
Bazon