From ed7f2503ea1b33fadb8f6aa5a538473ef3c58cab Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 25 Jan 2010 12:47:40 +0000
Subject: Updated ARM port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1232 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/extractionMachdep.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'powerpc/extractionMachdep.v')

diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index 46c40cae..83fda76e 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -12,6 +12,9 @@
 
 (* Additional extraction directives specific to the PowerPC port *)
 
+(* Selection *)
+Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)".
+
 (* Asm *)
 Extract Constant Asm.low_half => "fun _ -> assert false".
 Extract Constant Asm.high_half => "fun _ -> assert false".
-- 
cgit