From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 2 Sep 2010 12:42:19 +0000
Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as
 destroyed (set to Vundef) across   operations in the semantics of LTL, LTLin,
 Linear and Mach,   allowing Asmgen to reuse them. - Added IA32 port. -
 Cleaned up float conversions and axiomatization of floats.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 driver/Driver.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'driver')

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 4f98be2..56bdb01 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -235,7 +235,7 @@ Code generation options:
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
 Tracing options:
   -dparse        Save C file after parsing and elaboration in <file>.parse.c
-  -dcmedium      Save generated Cmedium in <file>.medium.c
+  -dc            Save generated Compcert C in <file>.compcert.c
   -dclight       Save generated Clight in <file>.light.c
   -dasm          Save generated assembly in <file>.s
 Linking options:
@@ -312,7 +312,7 @@ let cmdline_actions =
   "-o$", String(fun s -> exe_name := s);
   "-stdlib$", String(fun s -> stdlib_path := s);
   "-dparse$", Set option_dparse;
-  "-dcmedium$", Set option_dcmedium;
+  "-dc$", Set option_dcmedium;
   "-dclight$", Set option_dclight;
   "-dcminor", Set option_dcminor;
   "-drtl$", Set option_drtl;
-- 
cgit v1.2.3