aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Driver.ml')
-rw-r--r--driver/Driver.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b6224c32..5d4c2f9c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -108,7 +108,7 @@ let parse_c_file sourcename ifile =
end;
(* Conversion to Csyntax *)
let csyntax =
- match C2C.convertProgram ast with
+ match Timing.time "CompCert C generation" C2C.convertProgram ast with
| None -> exit 2
| Some p -> p in
flush stderr;