diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 09:34:59 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 09:34:59 +0100 |
commit | 76d51c51befc755d3ead6414c9609132189456e9 (patch) | |
tree | 877fe4a797c5aa47cb9ac0126daf850081a00b53 /lib/aux_file.ml | |
parent | baceb85e7e8efd5c8226a390d7d76f047f0920d5 (diff) | |
parent | d547a0424e3dea7d4affda0dd5428425786a7a92 (diff) |
Merge PR #6636: Stop running duplicate Travis jobs on pull requests.
Diffstat (limited to 'lib/aux_file.ml')
0 files changed, 0 insertions, 0 deletions