aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.doc
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.doc')
-rw-r--r--Makefile.doc2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc
index c31d81c8b..6a81b292e 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -415,7 +415,7 @@ OCAMLDOCDIR=dev/ocamldoc
DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
- ./parsing/*.mli ./proofs/*.mli \
+ ./parsing/*.mli ./proofs/*.mli API/API.mli \
./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
# Defining options to generate dependencies graphs