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

[Andrea Vezzosi]

you mean the full "make test" ?

In any case, any suggestion on how to get the latex-related tests to
work? They never did for me.

On Thu, Mar 28, 2019 at 5:05 PM Andreas Abel <abela at chalmers.se> wrote:
>
> Folks,
>
> don't forget your manners:
>
>    - before pushing to master, run the testsuite through
>    - if you want travis take care of this, work with pull requests
>
> If you think you can predict whether the testsuite will run through
> cleanly after your changes, let me assure you, you are most likely
> wrong.  I have been there many times.
>
> Best,
> Andreas
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se
> http://www.cse.chalmers.se/~abela/
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev