diff options
Diffstat (limited to 'ia32/extractionMachdep.v')
| -rw-r--r-- | ia32/extractionMachdep.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/ia32/extractionMachdep.v b/ia32/extractionMachdep.v index 435dce2..3c6ee2e 100644 --- a/ia32/extractionMachdep.v +++ b/ia32/extractionMachdep.v @@ -12,3 +12,9 @@ (* Additional extraction directives specific to the IA32 port *) +Require SelectOp. + +(* SelectOp *) + +Extract Constant SelectOp.symbol_is_external => + "fun id -> Configuration.system = ""macosx"" && C2C.atom_is_extern id". |