[Agda] permanently changing the Agda font

[J.Burton at brighton.ac.uk]

At Tue, 15 Sep 2009 12:54:33 +0200,
Wolfgang Jeltsch wrote:
> 
> Hello,
> 
> 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?
>

Hi, if you use the darcs emacs-mode you can customize the group, edit
Agda2 Highlight Face Groups and select "Use simplified highlighting
and default font-lock faces." Saving this choice edits your init file
and agda-mode will use your default fonts and colour theme.

Jim 
> Best wishes,
> Wolfgang
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda