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). --- checker/check.mllib | 2 ++ checker/checker.ml | 1 + 2 files changed, 3 insertions(+) (limited to 'checker') diff --git a/checker/check.mllib b/checker/check.mllib index 22df375623..8381144e89 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 ffe1553197..360f996499 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 -- cgit v1.2.3