From 1ecaed675113ccd366cf828ab2743a347bac72d3 Mon Sep 17 00:00:00 2001
From: Prashanth Mundkur
Date: Fri, 12 Jun 2020 09:12:55 -0700
Subject: Use output file for generated branch information.

---
 src/jib/c_backend.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/jib/c_backend.mli')

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 *)
 
-- 
cgit v1.2.3