From 95e723892c336808aad0926c675f3e0ac8ba7d99 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 8 Feb 2019 14:10:22 +0100
Subject: Remove global output_native_objects flag.

---
 library/declaremods.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library/declaremods.ml')

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
-- 
cgit v1.2.3