search

eddiefullmetal / gnome-shell-extensions

Various extensions for the gnome-shell
23 stars 12 forks source link

Add a delay on autohide feature. #10

Closed mathematicalcoffee closed 11 years ago

mathematicalcoffee commented 11 years ago

This was meant to be a pull request on eddiefullmetal/gnome-shell-extensions#6 but I couldn't work out how to add it to that issue rather than creating a new one.

Basically added a constant PANEL_DELAY_MS up the top of extension.js (currently set to 200ms) such that if the cursor is in the trigger area for less than that time, the panel will not open.

Unsure if you want to add this option to the panel-settings popup menu or whether you want to keep it a little more hidden; if you do want to add it to the popup menu, I have a PopupMenuSlider + label class in eddiefullmetal/gnome-shell-extensions#9 that could be used (I'm happy to do the code myself if you want this setting in the popup menu).

mathematicalcoffee commented 11 years ago

Withdrawing the pull request as there were issues where the panel would hide even when the cursor was on it that I haven't fixed yet.