From 0e40a5b6ae0997b11469fdeea702db4c7f878c17 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 15 Dec 2015 14:34:57 +0100
Subject: Print cfi_sections only if cfi is supported.

On older version of the binutils the cfi directives  are not always
supported so we only print cfi_sections if the corresponding .ini
setting is set to true.
---
 backend/PrintAsmaux.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'backend/PrintAsmaux.ml')

diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 4a612c26..0ca5b8e0 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -129,6 +129,12 @@ let cfi_rel_offset =
   else
     (fun _ _ _ -> ())
 
+let cfi_section =
+  if Configuration.asm_supports_cfi then
+    (fun oc -> fprintf oc "	.cfi_sections	.debug_frame\n")
+  else
+    (fun _ -> ())
+
 (* Basic printing functions *)
 let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
-- 
cgit