Ubuntu
gnome-shell-extensions package

  1. Bug #1566091
  2. Comment #7

Comment 7 for bug 1566091

Revision history for this message
Jeremy Bícha (jbicha) wrote :

J. J., do you have any experience with git? It would be really useful if you could forward a Git patch for this issue to GNOME.