aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-01-31 09:09:28 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-12 17:20:35 +0100
commit5268efdefb396267bfda0c17eb045fa2ed516b3c (patch)
treeb27a12e165d2c5b8c1b4d3171f961b8a5025bbb3 /checker
parente03513b7309008a45957609739bcdaf3789f3052 (diff)
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).
Diffstat (limited to 'checker')
-rw-r--r--checker/check.mllib2
-rw-r--r--checker/checker.ml1
2 files changed, 3 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 22df37562..8381144e8 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -33,6 +33,8 @@ Util
Ephemeron
Future
CUnix
+
+Systemdirs
System
Profile
RemoteCounter
diff --git a/checker/checker.ml b/checker/checker.ml
index ffe155319..360f99649 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -10,6 +10,7 @@ open Pp
open Errors
open Util
open System
+open Systemdirs
open Flags
open Names
open Check