-
Mathieu Giraud authored
This is more generic than what was previously in the development menu. Applied to 'highlight menu' in js/segmenter.js.
f715996f
This is more generic than what was previously in the development menu. Applied to 'highlight menu' in js/segmenter.js.