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

This commit is contained in:
Tor Hedin Brønner 2019-03-10 02:44:20 +01:00 committed by Jan Tojnar
parent 51e7d0bda8
commit b6589686c4
No known key found for this signature in database
GPG Key ID: 7FAB2A15F7A607A4

View File

@ -2,13 +2,13 @@
stdenv.mkDerivation rec { stdenv.mkDerivation rec {
name = "gnome-shell-extension-remove-dropdown-arrows-${version}"; name = "gnome-shell-extension-remove-dropdown-arrows-${version}";
version = "9"; version = "11";
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 = "1z9icxr75rd3cas28xjlmsbbd3j3sm1qvj6mp95jhfaqj821q665"; sha256 = "1g99r9bpjdhab3xj74wkl40gdnaf2w51kswcr8mi6bq72n4wjxwh";
}; };
# 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