aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Driver.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-19 17:24:01 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-19 17:24:01 +0100
commit959542e4cf126c4f46f00c764b5365804de637c6 (patch)
tree58eb44d941b65d15537a5c53bccd8257030aadf2 /driver/Driver.ml
parentb0c09b32f3e559ca22afc4dc40fdd60964cb3292 (diff)
parentb0eb1dfc9fd7b15c556c49101390d882b0f00f8a (diff)
downloadcompcert-959542e4cf126c4f46f00c764b5365804de637c6.tar.gz
compcert-959542e4cf126c4f46f00c764b5365804de637c6.zip
Merge github.com:AbsInt/CompCert into compcert_windows
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;