diff options
| author | Alasdair Armstrong | 2018-12-14 15:17:42 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-12-14 15:17:42 +0000 |
| commit | 2dfcbdeedb0ac40d4865aaf5c2202dfba95f4a38 (patch) | |
| tree | e267b9d9166e3548f71508d9d68b8ea1f35a304d /src/process_file.ml | |
| parent | bfb20a209d1b72c832b4376d6d3c51d39970ef2f (diff) | |
Add a few more tests for Jenkins
Some of the output from the tests scripts is odd on Jenkins, try to
fix this by flushing stdout more regularly in the test scripts
Diffstat (limited to 'src/process_file.ml')
0 files changed, 0 insertions, 0 deletions