Joe, I think bug 828751 will be fixed soon which should fix things without needing to create a gnome-shell patch, which we'd then have to drop again.
Joe, I think bug 828751 will be fixed soon which should fix things without needing to create a gnome-shell patch, which we'd then have to drop again.