You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The old names for the coverage elements (highlights) is quite confusing now that we have gutter coverage elements as well as line and map based ones. We can use the example naming by @DevilXD as a starting point for switching to something more sensical.
Work
Slightly adjust the settings names to make more sense regarding their visual nature.
Figure out if this change should be in the next minor release or next major (changing the setting name will probably mean a breaking change unless we deprecate the old value and use it as the default for folks that have set it)
The text was updated successfully, but these errors were encountered:
Reference
#239 (comment)
Problem
The old names for the coverage elements (highlights) is quite confusing now that we have gutter coverage elements as well as line and map based ones. We can use the example naming by @DevilXD as a starting point for switching to something more sensical.
Work
The text was updated successfully, but these errors were encountered: