PR# 12134 Auto Hide button should have different tooltips for enable/disable

Problem Report Summary
Submitter: prestoat2000
Category: EiffelStudio
Priority: Medium
Date: 2007/02/25
Class: Bug
Severity: Non-critical
Number: 12134
Release: 6.0.66833
Confidential: No
Status: Closed
Responsible:
Environment: Mozilla/5.0 (X11; U; SunOS i86pc; en-US; rv:1.8.1) Gecko/20061228 Firefox/2.0 Solaris 10 on x64
Synopsis: Auto Hide button should have different tooltips for enable/disable

Description
The Auto Hide button should have separate tooltips, depending on whether
clicking the button will enable or disable auto hiding.  I suggest either

   Auto Hide, Disable Auto Hide
   Enable Auto Hide, Disable Auto Hide

I think I prefer the former pair.
To Reproduce

										
Problem Report Interactions
From:larryl    Date:2007/03/27    Status: Closed    Download   
At revision#67582, we start to use "Auto Hide" and "Disable Auto Hide" for the pin buttons' tool tips.

Thanks for your report.