diff options
| author | Hugo Herbelin | 2015-01-31 09:09:28 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-12 17:20:35 +0100 |
| commit | 5268efdefb396267bfda0c17eb045fa2ed516b3c (patch) | |
| tree | b27a12e165d2c5b8c1b4d3171f961b8a5025bbb3 /Makefile.build | |
| 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.build')
| -rw-r--r-- | Makefile.build | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index 0d87d98e96..6c3834ae43 100644 --- a/Makefile.build +++ b/Makefile.build @@ -606,6 +606,7 @@ tools: $(TOOLS) $(DEBUGPRINTERS) $(COQDEPBOOT) # coqdep_boot. COQDEPBOOTSRC:= \ + lib/systemdirs.mli lib/systemdirs.ml \ tools/coqdep_lexer.mli tools/coqdep_lexer.ml \ tools/coqdep_common.mli tools/coqdep_common.ml \ tools/coqdep_boot.ml |