[Agda] Agda and Aquamacs

Nils Anders Danielsson nils.anders.danielsson at gmail.com
Thu Jun 19 19:05:00 CEST 2008


On Thu, Jun 19, 2008 at 4:39 PM, Sean Leather <sean.leather at gmail.com> wrote:
>
> This does work around the problem. I did that before learning about the
> "change default" setting. It added an extra step to opening every file, and
> that's what sparked my initial question.

It is arguably bad behaviour for the Agda mode to change the frame's
default font (hence the agda2-change-default-font setting). I still
think it is useful to do this, though, since the default default font
is often inadequate. Maybe someone more Emacs-savvy knows a better way
to accomplish our goals?

-- 
/NAD


More information about the Agda mailing list