diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-23 10:53:41 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-23 11:11:15 +0100 |
| commit | d547a0424e3dea7d4affda0dd5428425786a7a92 (patch) | |
| tree | 7783e5859d78891b603c6d91c38985561555be5e /lib/aux_file.ml | |
| parent | 2e798fb83db743ce44350af6f7f9442811f374ad (diff) | |
Stop running duplicate Travis jobs on pull requests.
These tests are already done by CircleCI.
Diffstat (limited to 'lib/aux_file.ml')
0 files changed, 0 insertions, 0 deletions