[julia-users] is the highlight color in docs selectable

[Jeffrey Sarnoff]

Reading docs peppered with red is bit headache inducing for me.  Is there
 support for a less aggressive color?