This is really a follow-up to #401, so feel free to condense. I see that the documentation has been corrected to show that the defaults for color.highlight.background and color.hover.background are "#D2E5FF". Unfortunately, it now shows the default for color.background as "#D2E5FF", which is not correct. The previous value of "#97C2FC" WAS the correct one.
This is really a follow-up to #401, so feel free to condense. I see that the documentation has been corrected to show that the defaults for
color.highlight.backgroundandcolor.hover.backgroundare "#D2E5FF". Unfortunately, it now shows the default forcolor.backgroundas "#D2E5FF", which is not correct. The previous value of "#97C2FC" WAS the correct one.