diff options
Diffstat (limited to 'Makefile.doc')
-rw-r--r-- | Makefile.doc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.doc b/Makefile.doc index 1b0803f19..8cb9c9f0f 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -387,7 +387,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 API/API.mli \ + ./parsing/*.mli ./proofs/*.mli \ ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) # Defining options to generate dependencies graphs |