[ jEdit-devel ] [ jedit-Plugin Bugs-1793585 ] GlobalPlugin: Jump immediately if # of results=1

[SourceForge.net <no...@so...>]

Plugin Bugs item #1793585, was opened at 2007-09-13 02:41
Message generated for change (Comment added) made by shlomy
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=565475&aid=1793585&group_id=588

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: None
Group: None
>Status: Closed
>Resolution: Fixed
Priority: 5
Private: No
Submitted By: Alan Ezust (ezust)
Assigned to: Shlomy Reinstein (shlomy)
Summary: GlobalPlugin: Jump immediately if # of results=1

Initial Comment:
If the # of results for definitions or references is 1, it should just jump to the definition or reference immediately without waiting for me to select it.

Maybe this should be an option people can switch off, but I can't imagine wanting it off, so the default should be TRUE.





----------------------------------------------------------------------

>Comment By: Shlomy Reinstein (shlomy)
Date: 2007-09-13 07:58

Message:
Logged In: YES 
user_id=1477607
Originator: NO

Fixed in SVN revision 10565.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=565475&aid=1793585&group_id=588