From 1e24932c5f5badcca3125b9c4c0df2ac113532bf Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 3 Mar 2010 13:16:21 +0000
Subject: Suppressed Init_pointer, now useless.  Improved printing of strings
 in generated .s

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

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index fa1d048..0388c2e 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -383,10 +383,6 @@ let print_init p = function
       if ofs = 0l
       then fprintf p "&%s,@ " (extern_atom symb)
       else fprintf p "(void *)((char *)&%s + %ld),@ " (extern_atom symb) ofs
-  | Init_pointer id ->
-      match string_of_init id with
-      | None -> fprintf p "/* pointer to other init*/,@ "
-      | Some s -> fprintf p "%a,@ " print_escaped_string s
 
 let print_globvar p (Coq_pair(Coq_pair(id, init), ty)) =
   match init with
-- 
cgit v1.2.3