--- Day changed Thu Aug 31 2017
WilliamHamilton[hi, I have a question about the latex exporter: when trying to compile an agda-generated tex file, I get this error:31/08 11:32
WilliamHamilton[! LaTeX Error: Command \textGamma unavailable in encoding T1.31/08 11:32
WilliamHamilton[In the latest agda manual for latex generation, it's mentioned that in case of missing characters, one should add them manually via something like `\DeclareUnicodeCharacter{8988}{\ensuremath{\ulcorner}}`31/08 11:34
WilliamHamilton[two question though: is this actually the reason for the error? and how do I get the correct number (like 8988)?31/08 11:35
WilliamHamilton[mietek mabye ^31/08 11:39
SaizanWilliamHamilton[: \usepackage{textgreek} maybe, are you \usepackage{agda} ?31/08 12:39
WilliamHamilton[thanks Saizan, that solved the issue. Do you have preferences/guidelines on pdflatex/xetex when rendering agda?31/08 12:45
WilliamHamilton[(I was missing textgreek)31/08 12:45
SaizanI think pdflatex might be the more used, but i don't use agda --latex that much31/08 12:50
WilliamHamilton[perfect, thanks again31/08 12:50

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!