eddiefullmetal/gnome-shell-extensions — pull request #10 by mathematicalcoffee (2012-10-05 02:16:44+00:00)
Title: Add a delay on autohide feature.

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).