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

[Andreas Abel]

 > you mean the full "make test" ?

Yes.

 > In any case, any suggestion on how to get the latex-related tests to
 > work?

Do you have the texlive suite 2018 installed?  (I suppose so.)

On 2019-04-08 20:09, Andrea Vezzosi wrote:
> 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

-- 
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/