diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-04 18:35:40 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-01-04 18:35:40 +0100 |
| commit | 8219490aae44fa79932d913cc69941d6b22a70a3 (patch) | |
| tree | b60527a283191e2293a4af3497e48303402ee626 /cparser/Cprint.ml | |
| parent | b1455cc40ebf6bb00722ff128e702f83c9b4dca8 (diff) | |
| download | compcert-kvx-8219490aae44fa79932d913cc69941d6b22a70a3.tar.gz compcert-kvx-8219490aae44fa79932d913cc69941d6b22a70a3.zip | |
Handle dcompcertc and dparsedc like all dump opts.
This time with the correct place for setting the destination files.
Bug 20521
Diffstat (limited to 'cparser/Cprint.ml')
| -rw-r--r-- | cparser/Cprint.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 0a927873..d623ab96 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -555,3 +555,13 @@ let program pp prog = fprintf pp "@[<v 0>"; List.iter (globdecl pp) prog; fprintf pp "@]@." + +let destination : string option ref = ref None + +let print_if prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out f in + program (formatter_of_out_channel oc) prog; + close_out oc |