diff options
| author | Alasdair Armstrong | 2020-06-12 17:36:58 +0100 |
|---|---|---|
| committer | GitHub | 2020-06-12 17:36:58 +0100 |
| commit | 81895cb3af440536c5a8b86136c3de1836d5098a (patch) | |
| tree | d616eff4b72835e7462e77058ba226337c6e8a1d /src/jib/c_backend.mli | |
| parent | e93b34914e70d8590fa86c81577fbe723236c086 (diff) | |
| parent | 1ecaed675113ccd366cf828ab2743a347bac72d3 (diff) | |
Merge pull request #70 from rems-project/branch-info-output-file
Use output file for generated branch information.
Diffstat (limited to 'src/jib/c_backend.mli')
| -rw-r--r-- | src/jib/c_backend.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli index b10e53d3..5f2d5211 100644 --- a/src/jib/c_backend.mli +++ b/src/jib/c_backend.mli @@ -88,7 +88,7 @@ val opt_prefix : string ref val opt_extra_params : string option ref val opt_extra_arguments : string option ref -val opt_branch_coverage : bool ref +val opt_branch_coverage : out_channel option ref (** Optimization flags *) |