Skip to content
Success

Changes

Summary

  1. clarified names (again), e.g. relevant for "Plugin Options";
Changeset 74052:f34d54b0e5de by wenzelm:
clarified names (again), e.g. relevant for "Plugin Options";
The file was modified src/Tools/jEdit/jedit_main/plugin.props (diff)