diff options
| author | Emilio Jesus Gallego Arias | 2019-01-23 17:14:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-23 17:14:42 +0100 |
| commit | f5241b99bb15f019eb629a7f24f2993f011e7e06 (patch) | |
| tree | 2066732dc4032d6bc1f1f07baf66a3e0dd14390f | |
| parent | 09b7c512dcdc66f2cc9082046a5e1fb97bf7336a (diff) | |
| parent | 1e0d3028402080d449ce5a84bf20cba221cc8f0b (diff) | |
Merge PR #9357: Fix recursive loadpath of ML files
Reviewed-by: ejgallego
| -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 |