From b5690cc9fec033940a115c97e8b303b2b5f7312a Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Wed, 1 Dec 2021 19:02:55 +0100 Subject: [PATCH] [dev] ensures the devman is up-to-date before checking coherence with comments --- Makefile | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 27e3a6e2ef2..8e1fd43895e 100644 --- a/Makefile +++ b/Makefile @@ -1712,8 +1712,11 @@ $(CHECK_API_DIR)/check_code.cmxs: $(CHECK_API_DIR)/check_code.ml CHECK_CODE=$(CHECK_API_DIR)/check_code.cmxs -.PHONY: check-devguide -check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc +.PHONY: check-devguide devguide +devguide: + $(MAKE) FRAMAC_INTERNAL=no -C $(DOC_DEV_DIR) + +check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc devguide $(PRINT) 'Checking developer guide consistency' $(MKDIR) $(CHECK_API_DIR)/html $(OCAMLDOC) $(DOC_FLAGS) -I $(OCAMLLIB) \ -- GitLab