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