Plugin Manager Install Pane Filter Field

jEdit is a programmer's text editor written in Java.

Brought to you by: daleanson, ezust, grepppo, k_satoda, and 5 others

#172 Plugin Manager Install Pane Filter Field

Milestone: v5.2

Status: closed-fixed

Owner: nobody

Labels: None

Priority: 5

Updated: 2014-03-24

Created: 2007-10-03

Creator: Frank

Private: No

I would appreciate if by typing the first letters of a plug in name, the selection would jump to the plug in.

Discussion

Alan Ezust - 2014-03-24

summary: Plugins Manager navigation --> Plugin Manager Install Pane Filter Field

Description has changed:

Diff:

--- old +++ new @@ -1,4 +1,2 @@ I would appreciate if by typing the first letters of a plug in name, the selection would jump to the plug in. -By the way the same is valid for all lists and trees. -\(the help tree for instance\)

status: open --> closed-fixed

Group: --> v5.2
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Alan Ezust - 2014-03-24

This is done in jEdit 5.0

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Log in to post a comment.