diff options
| author | Maxime Dénès | 2019-01-18 16:09:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-19 15:05:14 +0100 |
| commit | 1e0d3028402080d449ce5a84bf20cba221cc8f0b (patch) | |
| tree | b92691701f6c29c0a49a68429f9137ba15166247 /vernac/mltop.ml | |
| parent | b2877df2c79147bd2e26e53e43291b9b29a2aab8 (diff) | |
Fix recursive loadpath of ML files
ML files at the root were not taken into account. Coqdep was already
doing the right thing.
Diffstat (limited to 'vernac/mltop.ml')
| -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 |