gnomeExtensions.remove-dropdown-arrows: 11 -> 13

This commit is contained in:
worldofpeace
2019-10-03 00:09:15 +02:00
committed by Jan Tojnar
parent 4333119b64
commit d6413fc352
@@ -2,13 +2,13 @@
stdenv.mkDerivation rec { stdenv.mkDerivation rec {
pname = "gnome-shell-extension-remove-dropdown-arrows"; pname = "gnome-shell-extension-remove-dropdown-arrows";
version = "11"; version = "13";
src = fetchFromGitHub { src = fetchFromGitHub {
owner = "mpdeimos"; owner = "mpdeimos";
repo = "gnome-shell-remove-dropdown-arrows"; repo = "gnome-shell-remove-dropdown-arrows";
rev = "version/${version}"; rev = "version/${version}";
sha256 = "1g99r9bpjdhab3xj74wkl40gdnaf2w51kswcr8mi6bq72n4wjxwh"; sha256 = "09b2hnfbqym20pb1sfc8xiz7gs2kbs6b1s7xl8swc8dydhsbambk";
}; };
# This package has a Makefile, but it's used for publishing and linting, not # This package has a Makefile, but it's used for publishing and linting, not