aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/mltop.ml
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-04-08 20:12:36 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-04-09 22:50:36 +0200
commitb89502c9f2bf56ee89b7e280815c339ef7b8947c (patch)
tree35f9cd1d3371d52026e72c33c6b6c5480c05af27 /toplevel/mltop.ml
parent24ea28b87f0227582ae29ea6bb485812c6b641eb (diff)
Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fix for Rocq/Rational.)"
This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69. Conflicts: CHANGES
Diffstat (limited to 'toplevel/mltop.ml')
-rw-r--r--toplevel/mltop.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 458fe8ef0..196ab98ed 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -180,7 +180,6 @@ let add_rec_path ~unix_path ~coq_root ~implicit =
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 Loadpath.ImplicitPath dir in