[Agda] List of fonts required for Emacs mode?

[András Kovács]

I've only used "options->set default font" in the emacs menu bar, that sets
the font globally.

David Banas <capn.freako at gmail.com> ezt írta (időpont: 2020. júl. 29., Sze,
15:55):

> Okay, thanks.
>
> Do you, then, set the value of the *agda2-fontset-name* variable to <
> *DejaVu*/*Mononoki* proper font name>, as opposed to "fontset-agda2"?
>
> -db
>
>
> On Wed, Jul 29, 2020 at 2:47 AM András Kovács <puttamalac at gmail.com>
> wrote:
>
>> Hi,
>>
>> Strictly speaking, there isn't a required font, rather, people tend to
>> use monospace fonts with good unicode support.
>> I personally use DejaVu Sans Mono. The PLFA book recommends Mononoki
>> <https://plfa.github.io/GettingStarted/#using-mononoki-in-emacs>.
>>
>> David Banas <capn.freako at gmail.com> ezt írta (időpont: 2020. júl. 29.,
>> Sze, 1:26):
>>
>>> Hi,
>>>
>>> Would someone be so kind as to post the list of required fonts for the
>>> Agda Emacs mode?
>>> I can't seem to find them in the documentation.
>>>
>>> Thanks,
>>> -db
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200729/ea16ed00/attachment.html>