aboutsummaryrefslogtreecommitdiffstats
path: root/x86/extractionMachdep.v
diff options
context:
space:
mode:
Diffstat (limited to 'x86/extractionMachdep.v')
-rw-r--r--x86/extractionMachdep.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index a29553e8..1509878f 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.v
@@ -21,6 +21,8 @@ Require SelectOp ConstpropOp.
Extract Constant SelectOp.symbol_is_external =>
"fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id".
+Extract Constant SelectOp.favor_branchless =>
+ "fun () -> !Clflags.option_ffavor_branchless".
(* ConstpropOp *)