diff options
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 |