diff options
| author | Jim Fehrle | 2018-05-18 12:03:19 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2018-07-23 08:25:11 -0700 |
| commit | a6131723faa8699e485a88fae8cc2323b82a8461 (patch) | |
| tree | adffb12de7e173d3a948976fd1b6de669be2bf77 /lib/pp_diff.mli | |
| parent | 496d9d4007f59e6114dae9a94ee5a39d241484cf (diff) | |
Make the out_channel for the log file accessible so tests can write to it (e.g. for debugging)
Diffstat (limited to 'lib/pp_diff.mli')
0 files changed, 0 insertions, 0 deletions