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

[Nils Anders Danielsson]

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