aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Cprint.mli
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-01-04 18:35:40 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-01-04 18:35:40 +0100
commit8219490aae44fa79932d913cc69941d6b22a70a3 (patch)
treeb60527a283191e2293a4af3497e48303402ee626 /cparser/Cprint.mli
parentb1455cc40ebf6bb00722ff128e702f83c9b4dca8 (diff)
downloadcompcert-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.mli')
-rw-r--r--cparser/Cprint.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/cparser/Cprint.mli b/cparser/Cprint.mli
index fe71e4fe..be7ce029 100644
--- a/cparser/Cprint.mli
+++ b/cparser/Cprint.mli
@@ -33,3 +33,6 @@ val storage : Format.formatter -> C.storage -> unit
val field : Format.formatter -> C.field -> unit
val globdecl : Format.formatter -> C.globdecl -> unit
val program : Format.formatter -> C.program -> unit
+
+val destination : string option ref
+val print_if : C.program -> unit