Add option to use bold text in terminals

[ericcornelissen]

Closes #182

Adds a toggle to the Terminal Page to enable/disable bold text in terminals. Currently, from my testing, when BoldText is enabled there is no real distinction between normal and bold text in most fonts, I also addressed this in this comment.

Alternative implementation

Currently the conversion from boolean to fontWeight and fontWeightBold value is performed 2x each, alternatively we could use transformer functions, e.g. ⬇️, but this seems like overkill to me.

term.setOption('fontWeight', boldToFontWeight(options.boldText));
term.setOption('fontWeightBold', boldToFontWeightBold(options.boldText));

...

function boldToFontWeight(boldText) {
  return options.boldText ? 'bold' : 'normal';
}
function boldToFontWeightBold(boldText) {
  return options.boldText ? 'bolder' : 'bold';
}

[ericcornelissen]

The build failure seems to be caused by the certificate being invalid, the same is true for the latest build on master even though the certificate was updated in that commit for #185 🤔

[felixse]

That's my fault. The CI is using some encrypted certificates I should also have updated, but my plan is to migrate the CI to Azure Pipelines in the next days.