Closed giordano closed 5 years ago
@giordano If you want to make it clearer which commits are specific to this PR, you can also change the target branch so that it's the one from #376.
Although that would then mean that this should be merged first, and then #376 (as updated by this).
While reviewing this PR we found the problem reported in #385, but this can be merged before fixing that since the problem only occurs in very specific cases.
This will automatically update the font of the related line numbers, too. Fix #377. Fix #385.
Note: this is based on #376 and thus it should be merged after that PR. The reason it's based on that PR is because they contain conflicting changes. If you want to review this PR, just look at the last commit of the series.