gnomeExtensions: move dropped extensions next to aliases
This commit is contained in:
parent
12a9bd6fb8
commit
1085727d81
@ -28882,10 +28882,10 @@ in
|
|||||||
window-corner-preview = callPackage ../desktops/gnome/extensions/window-corner-preview { };
|
window-corner-preview = callPackage ../desktops/gnome/extensions/window-corner-preview { };
|
||||||
window-is-ready-remover = callPackage ../desktops/gnome/extensions/window-is-ready-remover { };
|
window-is-ready-remover = callPackage ../desktops/gnome/extensions/window-is-ready-remover { };
|
||||||
workspace-matrix = callPackage ../desktops/gnome/extensions/workspace-matrix { };
|
workspace-matrix = callPackage ../desktops/gnome/extensions/workspace-matrix { };
|
||||||
|
} // lib.optionalAttrs (config.allowAliases or false) {
|
||||||
nohotcorner = throw "gnomeExtensions.nohotcorner removed since 2019-10-09: Since 3.34, it is a part of GNOME Shell configurable through GNOME Tweaks.";
|
nohotcorner = throw "gnomeExtensions.nohotcorner removed since 2019-10-09: Since 3.34, it is a part of GNOME Shell configurable through GNOME Tweaks.";
|
||||||
mediaplayer = throw "gnomeExtensions.mediaplayer deprecated since 2019-09-23: retired upstream https://github.com/JasonLG1979/gnome-shell-extensions-mediaplayer/blob/master/README.md";
|
mediaplayer = throw "gnomeExtensions.mediaplayer deprecated since 2019-09-23: retired upstream https://github.com/JasonLG1979/gnome-shell-extensions-mediaplayer/blob/master/README.md";
|
||||||
} // lib.optionalAttrs (config.allowAliases or false) {
|
|
||||||
unite-shell = gnomeExtensions.unite; # added 2021-01-19
|
unite-shell = gnomeExtensions.unite; # added 2021-01-19
|
||||||
arc-menu = gnomeExtensions.arcmenu; # added 2021-02-14
|
arc-menu = gnomeExtensions.arcmenu; # added 2021-02-14
|
||||||
};
|
};
|
||||||
|
Loading…
x
Reference in New Issue
Block a user