From 7d3ce4012a53b123dac95381bf46aac65f865d69 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Apr 2014 19:36:55 +0200
Subject: Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with
 -R. (Fix for Rocq/Rational.)

---
 CHANGES           | 3 ---
 toplevel/mltop.ml | 1 +
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/CHANGES b/CHANGES
index 48b39a01fb..ceabc053dc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -97,9 +97,6 @@ Tools
 
 - Option -I now only adds directories to the ml path. To add to both
   the load path and the ml path, use -I -as.
-- Option -R no longer adds recursively to the ml path; only the root
-  directory is added. (Behavior with respect to the load path is
-  unchanged.)
 - Option -nois prevents coq/theories and coq/plugins to be recursively
   added to the load path. (Same behavior as with coq/user-contrib.)
 
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index cc9aa59aa4..e0cb2209d5 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -178,6 +178,7 @@ let add_rec_path ~unix_path ~coq_root =
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
+    let () = List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs in
     let () = add_ml_dir unix_path in
     let add (path, dir) = Loadpath.add_load_path path false dir in
     let () = List.iter add dirs in
-- 
cgit v1.2.3