[Agda-dev] Run the testsuite before pushing to master

[Andrea Vezzosi]

I installed the ubuntu (meta?) package texlive-full, which improved
things. However the xelatex tests still fail.

Following Nils' instructions I can get to an actual error:

! Undefined control sequence.
l.12 \newfontfamily
                   {\AgdaSerifFont}{Linux Libertine O}



On Tue, Apr 9, 2019 at 2:24 PM Nils Anders Danielsson <nad at cse.gu.se> wrote:
>
> On 09/04/2019 10.18, Andrea Vezzosi wrote:
> > I suppose some work, but for
> >
> > doc-user-manual-tools-acmart-pdflatex_LaTeX
> >
> > I get
> >
> > LATEX_COMPILE_FAILED with pdflatex
>
> It should be possible to get a more informative error message by running
> the following commands (starting in the root directory of the Agda
> source tree):
>
> cd doc/user-manual/tools
> agda --latex acmart-pdflatex.lagda.tex
> cd latex
> pdflatex acmart-pdflatex.tex
>
> --
> /NAD
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev