<div dir="ltr"><div><div><div><div class="">Min, thanks for explanation.<br></div><div class=""><div class=""> </div></div><br></div>Matthias, thanks. I looked in `styles.py` and I defined &quot;highlight_color&quot; style in the theme file I use, but it didn&#39;t change anything. I also tried &quot;color&quot; style, with same result. Then I tried by brute force to change the dict that get_colors() function (from `styles.py`) returns, by setting &quot;select&quot; key to &quot;#808080&quot; value. It didn&#39;t change anything again!?<br>
</div>I&#39;ll try harder in next couple of minutes and report back when I find the right variable :)<br><br></div>Cheers<br></div>