
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Oh, I see. So, you’ve left the <font face="Menlo" class=""><b class="">agda2-fontset-name</b></font> variable at its default value: <font face="Menlo" class="">nil</font>, then?<div class=""><br class=""></div><div class="">I guess I went too deep and should’ve taken the simpler path; D’oh! ;-)</div><div class=""><br class=""></div><div class="">Thanks!</div><div class="">-db</div><div class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jul 29, 2020, at 8:42 AM, András Kovács <<a href="mailto:puttamalac@gmail.com" class="">puttamalac@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">I've only used "options->set default font" in the emacs menu bar, that sets the font globally.</div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">David Banas <<a href="mailto:capn.freako@gmail.com" class="">capn.freako@gmail.com</a>> ezt írta (időpont: 2020. júl. 29., Sze, 15:55):<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr" class="">Okay, thanks.<div class=""><br class=""></div><div class="">Do you, then, set the value of the <font face="monospace" class=""><b class="">agda2-fontset-name</b></font> variable to <font face="monospace" class=""><<i class="">DejaVu</i>/<i class="">Mononoki</i> proper font name></font>, as opposed to "fontset-agda2"?</div><div class=""><br class=""></div><div class="">-db</div><div class=""><br class=""></div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Jul 29, 2020 at 2:47 AM András Kovács <<a href="mailto:puttamalac@gmail.com" target="_blank" class="">puttamalac@gmail.com</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr" class="">Hi,<div class=""><br class=""></div><div class="">Strictly speaking, there isn't a required font, rather, people tend to use monospace fonts with good unicode support. </div><div class="">I personally use DejaVu Sans Mono. The PLFA book <a href="https://plfa.github.io/GettingStarted/#using-mononoki-in-emacs" target="_blank" class="">recommends Mononoki</a>. </div></div><br class=""><div class="gmail_quote"><div dir="ltr" class="gmail_attr">David Banas <<a href="mailto:capn.freako@gmail.com" target="_blank" class="">capn.freako@gmail.com</a>> ezt írta (időpont: 2020. júl. 29., Sze, 1:26):<br class=""></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr" class="">Hi,<div class=""><br class=""></div><div class="">Would someone be so kind as to post the list of required fonts for the Agda Emacs mode?</div><div class="">I can't seem to find them in the documentation.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">-db</div><div class=""><br class=""></div></div>

_______________________________________________<br class="">

Agda mailing list<br class="">

<a href="mailto:Agda@lists.chalmers.se" target="_blank" class="">Agda@lists.chalmers.se</a><br class="">

<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank" class="">https://lists.chalmers.se/mailman/listinfo/agda</a><br class="">

</blockquote></div>

</blockquote></div>

</blockquote></div>

</div></blockquote></div><br class=""></div></body></html>