Chronological Thread 

< Chronological >      < Thread >

---

On Sunday 16 December 2001 23:41, Sebastian C. B. Sauer wrote:
> Is there an easy way of changing the menu bar font? I would much prefer
> having a sans-serif font for the menu.

It depends on what is an easy way for you.

I had a look at TeXmacs source, and it seems that user interface widgets are
created using the default font defined in the display class.

So you will have to change this font. A quick look in TeXmacs initialization
files has not revealed any command used to set the default font, so I assume
you have to change the font defined in the source.

The default font is defined in src/Window/X/x_font.gen.cc in the
x_display_rep::default_font method (line 199).

Here you will find the following statement:
return tex_ec_font (this, "ecrm", 11, 300);

Just change "ecrm" to "ecss" to have TeXmacs use a sans-serif font. Of course
you will have to recompile an reinstall TeXmacs, but that's a very simple
business if you are used to the standard GNU installation system, also known
as "./configure && make && make install".

Changing the default font of the display will not affect the default font
used in documents.

I consider this to be easy, but I understand some people are not
confortable with tweaking source and recompiling software.

> so long,

And thanks for all the fish.

---

• changing the menu bar font, Sebastian C. B. Sauer, 12/16/2001
  • Re: changing the menu bar font, David Allouche, 12/17/2001
    • Re: changing the menu bar font, Sebastian C. B. Sauer, 12/17/2001
      • Re: changing the menu bar font, Joris van der Hoeven, 12/19/2001

---

Archive powered by MHonArc 2.6.19.