diff options
| author | Alasdair Armstrong | 2018-11-16 16:26:35 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-11-16 16:26:35 +0000 |
| commit | b3ea287bcf8be43714595b6921a0c47d25a67eee (patch) | |
| tree | 84430f3cb6e68ceac9c127288b12c8ed3c9de157 /src/process_file.ml | |
| parent | 60bcce4648ed029ca3c19c023f5ca525b43eced4 (diff) | |
Various bugfixes and a simple profiling feature for rewrites
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index bb789d0a..53293849 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -364,8 +364,10 @@ let output libpath out_arg files = output1 libpath out_arg f defs) files -let rewrite_step defs (name,rewriter) = +let rewrite_step defs (name, rewriter) = + let t = Profile.start () in let defs = rewriter defs in + Profile.finish ("rewrite " ^ name) t; let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> begin |