From 8219490aae44fa79932d913cc69941d6b22a70a3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 4 Jan 2018 18:35:40 +0100
Subject: Handle dcompcertc and dparsedc like all dump opts.

This time with the correct place for setting the destination files.
Bug 20521
---
 driver/Driver.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'driver/Driver.ml')

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 5afa0a76..b23a4e4f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -76,7 +76,9 @@ let compile_c_file sourcename ifile ofile =
   (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
     dst := if !opt then Some (output_filename sourcename ".c" ext)
-                   else None in
+      else None in
+  set_dest Cprint.destination option_dparse ".parsed.c";
+  set_dest PrintCsyntax.destination option_dcmedium ".compcert.c";
   set_dest PrintClight.destination option_dclight ".light.c";
   set_dest PrintCminor.destination option_dcminor ".cm";
   set_dest PrintRTL.destination option_drtl ".rtl";
-- 
cgit