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

[Andres Sicard Ramirez]

Hi Andrea,

On Mon, 8 Apr 2019 at 13:09, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>
> In any case, any suggestion on how to get the latex-related tests to
> work? They never did for me.

They work for me. Which is your problem?

Best,

-- 
Andrés