Merge Issue #14876: Use user-selected font for highlight configuration.
Patch by Roger Serwy.