From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 10 Oct 2016 10:59:22 +0200 Subject: Put all plugins behind an "API". --- Makefile.doc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.doc') 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 -- cgit v1.2.3