Re: [paragui-users] changing the font size

[Vibhu Rishi]

Okay, found this out. Just putting it here for further reference from
other people.

The themes are stored in a .zip file. Example : default.zip. This file
should be somewhere that your paragui library expects if you want the
application to find it . On my Linux system it is in /usr/share/paragui
This file has a .theme file (e.g. default.theme) and a directory of the
same name. default.theme is an XML file which stores the information of
the themes. The directory has any bmp files you want and the font file
you want with the theme.
To change the font size, unzip the zip file, and edit the .theme file to
change the font size to what ever you want. I changed it from 14 to 10
and it works for me !
Don't forget to zip up everything again and replace the file in the
default search path.

Alternatively, you can chage the name of the zip file also, but you need
to make corresponding changes to the .theme file also.

have fun making games !!!

vibhu..

On Tue, 2002-05-14 at 17:53, Vibhu Rishi wrote:
> hi
> how do i change the font size ? as of now i am getting very big fonts
> and i want to change those to smaller fonts. My guess is that i need to
> change the theme... is that correct ? Is there some documentation on how
> to make a new theme ? 
> 
> ciao
> vibhu..
>