texmacs-users - [TeXmacs] Is there a way to change the focus box color?

Subject: mailing-list for TeXmacs Users

List archive

[TeXmacs] Is there a way to change the focus box color?

From: Amir Michail <address@hidden>
To: texmacs-users <address@hidden>
Subject: [TeXmacs] Is there a way to change the focus box color?
Date: Mon, 20 May 2019 08:59:51 -0400

Hello,

For “dark mode” document colors, cyan for the focus box is too bright. Is
there a way to change its color?

Also, it would be nice to hide the focus box altogether when you don’t need
it.

Amir

[TeXmacs] Is there a way to change the focus box color?, Amir Michail, 05/20/2019
- Re: [TeXmacs] Is there a way to change the focus box color?, Massimiliano Gubinelli, 05/21/2019

List archive

[TeXmacs] Is there a way to change the focus box color?