From eacc77c5816a00b99aaef0d5ff596a3078b0a208 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 27 Nov 2018 16:33:36 +0100
Subject: [lib] Remove leftover flag `print_mod_uid`

The whole `native_name_from_filename` business seems quite strange tho.
---
 lib/flags.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'lib/flags.mli')

diff --git a/lib/flags.mli b/lib/flags.mli
index e282d4ca8c..d883cf1e30 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -119,8 +119,6 @@ val default_inline_level : int
 (** When producing vo objects, also compile the native-code version *)
 val output_native_objects : bool ref
 
-(** Print the mod uid associated to a vo file by the native compiler *)
-val print_mod_uid : bool ref
-
+(** Global profile_ltac flag  *)
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
-- 
cgit v1.2.3