From c24a652789e15b33153c1d90c6869eb6e6e28040 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 7 Mar 2010 17:49:18 +0000
Subject: Handling of builtins, continued. PrintCsyntax, PrintAsm: improve
 printing of float literals.

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

(limited to 'driver')

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 2d8b026..2cc409f 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -63,7 +63,7 @@ let preprocess ifile ofile =
 let compile_c_file sourcename ifile ofile =
   (* Simplification options *)
   let simplifs =
-    "bec"           (* blocks, impure exprs, implicit casts: mandatory *)
+    "bec" (* blocks, impure exprs, implicit casts: mandatory *)
   ^ (if !option_fstruct_passing then "s" else "")
   ^ (if !option_fstruct_assign then "S" else "")
   ^ (if !option_fbitfields then "f" else "") in
@@ -325,6 +325,7 @@ let cmdline_actions =
 
 let _ =
   Cparser.Machine.config := Cparser.Machine.ilp32ll64;
+  Cparser.Builtins.set C2Clight.builtins;
   CPragmas.initialize();
   parse_cmdline cmdline_actions usage_string;
   if !linker_options <> [] 
-- 
cgit v1.2.3