diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 1 |
2 files changed, 1 insertions, 3 deletions
@@ -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 |