[Agda] Re: A patch to agda2-mode.el

[Nils Anders Danielsson]

On Fri, Sep 5, 2008 at 01:55, Makoto Takeyama
<makoto.takeyama at aist.go.jp> wrote:
>
> Yes.  The current default 9x15 does not have a matching Kanji font but
> 9x18 does (regardless of X or Windows).  While we here on win needed
> matching Kanji badly, I thought others would not prefer it to less
> lines of taller chars.

I think it is better if all systems have the same defaults (if
possible). Unless anyone disagrees I will change the default fontset
on other platforms to match the Windows' one.

-- 
/NAD