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.

---
 lib/flags.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 29406ef275..7b1da2ff0e 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -118,8 +118,5 @@ let inline_level = ref default_inline_level
 let set_inline_level = (:=) inline_level
 let get_inline_level () = !inline_level
 
-(* Native code compilation for conversion and normalization *)
-let output_native_objects = ref false
-
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
-- 
cgit v1.2.3