From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- tools/coqdep_common.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tools/coqdep_common.mli') diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index afc171cb..d9ca3ca8 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -11,7 +11,8 @@ val option_noglob : bool ref val option_slash : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norecdir_list : string list ref +val norec_dirs : string list ref +val norec_dirnames : string list ref val suffixe : string ref type dir = string option val ( // ) : string -> string -> string -- cgit v1.2.3