diff options
| author | Emilio Jesus Gallego Arias | 2019-02-08 18:54:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-08 18:54:13 +0100 |
| commit | d8cf6da35a1b1c697e8bd3017de607c4a2d89691 (patch) | |
| tree | 91246b016eddb78b63a91c9c6836257d6d0887eb /library/declaremods.ml | |
| parent | 92df98da23057a47a6cd2053618fd97efe54ba30 (diff) | |
| parent | 6e052101b827a0abef83bc6a54da83e30f70bc94 (diff) | |
Merge PR #9525: Remove global output_native_objects flag.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 8699583cdf..5fd11e187a 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -928,10 +928,10 @@ let append_end_library_hook f = let old_f = !end_library_hook in end_library_hook := fun () -> old_f(); f () -let end_library ?except dir = +let end_library ?except ~output_native_objects dir = !end_library_hook(); let oname = Lib.end_compilation_checks dir in - let mp,cenv,ast = Global.export ?except dir in + let mp,cenv,ast = Global.export ?except ~output_native_objects dir in let prefix, lib_stack = Lib.end_compilation oname in assert (ModPath.equal mp (MPfile dir)); let substitute, keep, _ = Lib.classify_segment lib_stack in |