[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