From 5268efdefb396267bfda0c17eb045fa2ed516b3c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 Jan 2015 09:09:28 +0100
Subject: Using same code for browsing physical directories in coqtop and
 coqdep. In particular: - abstracting the code using calls to Unix opendir,
 stat, and closedir, - uniformly using warnings when a directory does not
 exist (coqtop was   ignoring silently and coqdep was exiting via
 handle_unix_error).

---
 toplevel/coqtop.ml | 2 +-
 toplevel/mltop.ml  | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0b9bb2f2ee..ffdd846197 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 357c5482fd..ef2e62c3b5 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)
 
-- 
cgit v1.2.3