HighlightMagics: merge default languages with the user config languages...
HighlightMagics: merge default languages with the user config languages
* When configuring HighlightMagics, instead of replacing fully the
language dict by the user provided one, we merge both.