From 1e0d3028402080d449ce5a84bf20cba221cc8f0b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 18 Jan 2019 16:09:54 +0100
Subject: Fix recursive loadpath of ML files

ML files at the root were not taken into account. Coqdep was already
doing the right thing.
---
 vernac/mltop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/mltop.ml b/vernac/mltop.ml
index 8d6268753e..78e26c65d4 100644
--- a/vernac/mltop.ml
+++ b/vernac/mltop.ml
@@ -215,7 +215,7 @@ let add_vo_path ~recursive lp =
     let () = match lp.has_ml with
       | AddNoML -> ()
       | AddTopML -> add_ml_dir unix_path
-      | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs in
+      | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in
     let add (path, dir) =
       Loadpath.add_load_path path ~implicit dir in
     let () = List.iter add dirs in
-- 
cgit v1.2.3