search

zzrough / gs-extensions-drop-down-terminal

Drop Down Terminal extension for the Gnome Shell
https://extensions.gnome.org/extension/442/drop-down-terminal/
GNU General Public License v3.0
416 stars 91 forks source link

Add support for Gnome 3.30 #217

Closed davidsmd closed 6 years ago

davidsmd commented 6 years ago

Apparently 3.30 breaks some extensions. Pixel-saver's fix for it, pulled from dash to dock, looks like it's pretty short and seems to be working correctly on Ubuntu 18.10 with Gnome 3.30

https://github.com/deadalnix/pixel-saver/pull/174/commits/ea29c6db84412ace8d5f25a99abdfff5770efe6b

If I'm feeling ambitious in the next couple of days, I'll try to submit a PR.

anarchodin commented 6 years ago

I sent #219, which solved the issue on my machine. Haven't tested on old GNOMEs, though.

davidsmd commented 6 years ago

Nice! Tried it out locally here on 3.30, looks good to me. Will save me an awful lot of cursing. Thanks!

debek commented 6 years ago

@zzrough Can You update this repo?

zzrough commented 6 years ago

I'm in holidays, we'll do as soon as i can.

Le 21 septembre 2018 11:25:08 GMT+00:00, Daniel Debny notifications@github.com a écrit :

@zzrough Can You update this repo?

-- You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub: https://github.com/zzrough/gs-extensions-drop-down-terminal/issues/217#issuecomment-423500129

--S

zzrough commented 6 years ago

PR merged.