From f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 17 May 2013 08:18:07 +0000
Subject: Preliminary support for debugging info (-g).

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

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index f91dca66..897a2ee5 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -242,11 +242,11 @@ let rec expr p (prec, e) =
                 (camlint_of_coqint sz) (camlint_of_coqint al)
                 exprlist (true, args)
   | Ebuiltin(EF_annot(txt, _), _, args, _) ->
-      fprintf p "__builtin_annot@[<hov 1>(%S,@ %a)@]"
-                (extern_atom txt) exprlist (true, args)
+      fprintf p "__builtin_annot@[<hov 1>(%S%a)@]"
+                (extern_atom txt) exprlist (false, args)
   | Ebuiltin(EF_annot_val(txt, _), _, args, _) ->
-      fprintf p "__builtin_annot_val@[<hov 1>(%S,@ %a)@]"
-                (extern_atom txt) exprlist (true, args)
+      fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]"
+                (extern_atom txt) exprlist (false, args)
   | Ebuiltin(_, _, args, _) ->
       fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
   | Eparen(a1, ty) ->
-- 
cgit