Subject: |
Re: EDM: seeking larger menus and text editing widgets |
From: |
John William Sinclair <[email protected]> |
To: |
[email protected] |
Date: |
Thu, 05 Mar 2015 10:37:05 -0500 |
Hi Jon,
EDM does not explicitly specify fonts for the normal windows and menus.
To get the font you desire, do the following:
1) Choose a font
- do xlsfonts to get a list of possibilites
- for this example, suppose you choose
-misc-fixed-medium-r-normal--20-200-75-75-c-100-iso8859-1
2) Edit .Xresources in your home directory and add a line that reads
edm*fontList: -misc-fixed-medium-r-normal--20-200-75-75-c-100-*-*
3) Load the X resources with one of the following command:
xrdb ~/.Xresources (this discards existing
resources)
xrdb -merge ~/.Xresources (this keeps existing resources)
4) run edm
The menu font should now be fairly large.
You will have to include the xrdb command in some login file (e.g. .bashrc).
Best regards,
John Sinclair
On 03/04/2015 02:58 PM, [email protected] wrote:
In EDM, is there some way to make the menu larger, that appears when
you click on a menu button? It is easy in EDM to set the size of the
menu button and its text, but the menu (and its text) that appears
when we click the button is always the same size - which is
uncomfortably small on our 1680 x 1050 displays.
Likewise, the text editing widget that appears when we click on an
editable text control is also too small - we would like to
enlarge that too.
Jon Jacky
- References:
- EDM: seeking larger menus and text editing widgets jon
- Navigate by Date:
- Prev:
waveProc maintainer? Michael Davidsaver
- Next:
Re: waveProc maintainer? Andrew Johnson
- Index:
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
<2015>
2016
2017
2018
2019
2020
2021
2022
2023
2024
- Navigate by Thread:
- Prev:
EDM: seeking larger menus and text editing widgets jon
- Next:
Problem with HDF5 plugin for areaDetector Wilkins, Stuart
- Index:
1994
1995
1996
1997
1998
1999
2000
2001
2002
2003
2004
2005
2006
2007
2008
2009
2010
2011
2012
2013
2014
<2015>
2016
2017
2018
2019
2020
2021
2022
2023
2024
|