diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 3 |
2 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0b9bb2f2e..ffdd84619 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -455,7 +455,7 @@ let parse_args arglist = |"-compile-verbose" -> add_compile true (next ()) |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true |"-feedback-glob" -> Dumpglob.feedback_glob () - |"-exclude-dir" -> exclude_search_in_dirname (next ()) + |"-exclude-dir" -> Systemdirs.exclude_directory (next ()) |"-init-file" -> set_rcfile (next ()) |"-inputstate"|"-is" -> set_inputstate (next ()) |"-load-ml-object" -> Mltop.dir_ml_load (next ()) diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 357c5482f..ef2e62c3b 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -11,6 +11,7 @@ open Util open Pp open Flags open Libobject +open Systemdirs open System (* Code to hook Coq into the ML toplevel -- depends on having the @@ -155,7 +156,7 @@ let add_ml_dir s = | WithoutTop when has_dynlink -> keep_copy_mlpath s | _ -> () -(* For Rec Add ML Path *) +(* For Rec Add ML Path (-R) *) let add_rec_ml_dir unix_path = List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) |