diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-31 09:09:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-12 17:20:35 +0100 |
| commit | 5268efdefb396267bfda0c17eb045fa2ed516b3c (patch) | |
| tree | b27a12e165d2c5b8c1b4d3171f961b8a5025bbb3 /Makefile.common | |
| parent | e03513b7309008a45957609739bcdaf3789f3052 (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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index d752a5be9..f83d8b88c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -232,7 +232,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc -COQENVCMO:=lib/clib.cma lib/errors.cmo +COQENVCMO:=lib/clib.cma lib/errors.cmo lib/systemdirs.cmo COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo |