[Agda] permanently changing the Agda font
Nils Anders Danielsson
nad at Cs.Nott.AC.UK
Tue Sep 15 20:33:43 CEST 2009
On 2009-09-15 11:54, Wolfgang Jeltsch wrote:
> I have changed the default font of Emacs and stored this setting in my
> ~/.emacs file. When I restart Emacs, this font is used. However, when
> I open an Agda buffer, Agda overrules my decision. How can I
> permanently change the font for Agda?
M-x customize-group agda2, set "Agda2 Fontset Name" to "Do not change
the font".
Alternatively you can use Emacs 23, under which this behaviour is
disabled due to improved font handling.
--
/NAD
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
More information about the Agda
mailing list