[gps-devel] Tooltips timeout missing in preference panel.

[Pascal]

Hello,

Though tooltips timeout is present in GPS documentation (14.1. The Preferences Dialog), it isn't in preference panel.
GPS GPL 2015 for MacOS.
Preference panel shows only check box to display tooltip or not.
The timeout is quite short so tooltip is displayed over and is masking contextual menu with a right clic.
That is quite annoying.
I don't want to remove completely tooltip as they remain useful.
How to set a higher timeout value?

Thanks, Pascal.
http://blady.pagesperso-orange.fr

PS: this message was previously sent to gps-users at lists.adacore.com with no success.