Closed joseo closed 9 years ago
Bajo circunstancias aún no claras (pudiera ser el evento desencadenado cuando se actualizan las opciones del plugin) los elementos de interfaz del plugin, que están dentro de su panel anclado, se "duplican".
Al cambiarse las opciones del plugin se llamaba a un método que volvía dividir la interfaz de jEdit, insertando de nuevo la interfaz del plugin.
Bug corregido.
Bajo circunstancias aún no claras (pudiera ser el evento desencadenado cuando se actualizan las opciones del plugin) los elementos de interfaz del plugin, que están dentro de su panel anclado, se "duplican".