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/checker.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'checker/checker.ml') 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 -- cgit v1.2.3