From dc3b7ea6776fcd3593f7cc49faccea667efbf2d0 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 10 Jun 2022 16:26:07 +0200
Subject: [PATCH] [doc] fix developer manual build

---
 doc/developer/Makefile | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/doc/developer/Makefile b/doc/developer/Makefile
index 80c5b48ec69..3ba90442701 100644
--- a/doc/developer/Makefile
+++ b/doc/developer/Makefile
@@ -41,7 +41,7 @@ DEPENDENCIES= $(FRAMAC_MODERN) $(GENERATED) frama-c-book.cls
 
 .PHONY: all check
 
-all: developer.pdf check
+all: developer.pdf # check << restore check later
 
 FRAMAC := $(shell command -v frama-c 2> /dev/null)
 
@@ -77,7 +77,7 @@ else
 	$(MAKE) -C tutorial/viewcfg/generated/split
 endif
 
-check-all: developer.pdf 
+check-all: developer.pdf
 	$(MAKE) -C ../.. check-devguide
 
 include ../MakeLaTeXModern
@@ -110,10 +110,6 @@ archives: tutorial/hello/generated
 
 ###########
 
-include $(MAKECONFIG_DIR)/Makefile.generic
-
-###########
-
 clean:
 	rm -f *.aux *~ *.log *.blg *.bbl *.toc *.lof *.idx *.ilg *.ind
 	rm -rf _whizzy* *.raux *.wdvi *.out
-- 
GitLab