Sur les centaines d'extensions, doit pas en avoir des masses qui posent problème. C'est plus de la malchance de tomber sur une à problème. Souvent c'est celles qui ne sont plus maintenu.
Quand il te manque une commande:
Quand il te manque une commande:
yum provides gnome-shell-extension-tool
Elle est fournit par le paquet gnome-shell, donc c'est étonnant que tu ne l'ai pas. Le chemin complet est /usr/bin/gnome-shell-extension-tool mais /usr/bin est normalement dans le $PATH des utilisateurs.