diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d762a246e6..d6bd754783 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -772,9 +772,9 @@ let export ?except senv dir = } in let ast, values = - if !Flags.no_native_compiler then [], [||] - else + if !Flags.native_compiler then Nativelibrary.dump_library mp dir senv.env str + else [], [||] in let lib = { comp_name = dir; |