**Added:** None

**Changed:** None

**Deprecated:** None

**Removed:** None

**Fixed:**

* Fixed a bug when the pygments plugin was used by third party editors etc. 

**Security:** None