[Agda] Agda and Aquamacs

Sean Leather sean.leather at gmail.com
Thu Jun 19 08:14:46 CEST 2008


Hi,

On Thu, Jun 19, 2008 at 02:43, WILSON F.A.J. <frank.wilson at durham.ac.uk>
wrote:

>  In the options group (M-x customize-group RET agda2 RET)
> have you tried setting "Change Default Font" to "Don't change"?
> I could be wrong, but I think this will get rid of the behaviour
> you are describing.
>
That worked! It's now so much nicer to play with Agda. :)

> (Given Monaco is your default font, it should
> not need to be changed when loading agda files since it should
> have all the glyphs. I think....)
>
Yes, Monaco has all of the Unicode characters I've needed so far.

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080619/df0624fc/attachment.html


More information about the Agda mailing list