Some options should be grayed when not a

Brought to you by: set

#12 Some options should be grayed when not a

Milestone: Editor

Status: open

Owner: Salvador Eduardo Tropea

Labels: Other (26)

Priority: 3

Updated: 2013-01-11

Created: 2001-10-16

Private: No

Some options like editor local options should be grayed
if no editor is opened. It could help to avoid
confusion.