Rename externaltools -> m_externalToolsMenu and make it private
Description
Description
Details
Details
- Committed
dhaumann Jan 23 2019, 8:04 PM - Differential Revision
- D17971: Revive External Tools plugin
- Parents
- R40:dde3169d7d23: Factor out KateExternalToolsConfigWidget into separate file
- Branches
- Unknown
- Tags