diff options
author | 2018-01-30 09:34:59 +0100 | |
---|---|---|
committer | 2018-01-30 09:34:59 +0100 | |
commit | 76d51c51befc755d3ead6414c9609132189456e9 (patch) | |
tree | 877fe4a797c5aa47cb9ac0126daf850081a00b53 /plugins/funind/invfun.mli | |
parent | baceb85e7e8efd5c8226a390d7d76f047f0920d5 (diff) | |
parent | d547a0424e3dea7d4affda0dd5428425786a7a92 (diff) |
Merge PR #6636: Stop running duplicate Travis jobs on pull requests.
Diffstat (limited to 'plugins/funind/invfun.mli')
0 files changed, 0 insertions, 0 deletions