From 27a773bc072e274f72b79ba03d33bf84901ca80a Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Tue, 18 Apr 2017 11:04:06 +0200 Subject: [PATCH] [Makefile] only include Makefile.kernel in external mode `Makefile.kernel` is only needed in external compilation mode, and even there, for static linking only, an obsolete and soon-to-be-removed compilation target. Moreover, including it unconditionally trigger race conditions in internal mode. --- Makefile.generating | 11 ----------- share/Makefile.dynamic | 4 ++-- 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/Makefile.generating b/Makefile.generating index ee1ff790afe..e7e5f880b5e 100644 --- a/Makefile.generating +++ b/Makefile.generating @@ -45,16 +45,6 @@ share/Makefile.kernel: Makefile.generating share/Makefile.config share/Makefile. $(RM) $@ $(ECHO) "# This makefile was automatically generated." > $@ $(ECHO) "# Do not modify." >> $@ - $(ECHO) "ifeq (\$$(FRAMAC_INTERNAL),yes)" >> $@ - $(ECHO) "DYN_BLINKFLAGS=$(filter-out $(INCLUDES),$(BLINKFLAGS)) $(foreach d,$(INCLUDES:-I%=%),-I $(FRAMAC_ROOT_SRCDIR)/$(d))" >> $@ - $(ECHO) "DYN_GEN_BYTE_LIBS=$(addprefix $(FRAMAC_ROOT_SRCDIR)/,$(GEN_BYTE_LIBS))" >> $@ - $(ECHO) "DYN_BYTE_LIBS=$(filter-out $(GEN_BYTE_LIBS),$(BYTE_LIBS))" >> $@ - $(ECHO) "DYN_ALL_BATCH_CMO=$(addprefix $(FRAMAC_ROOT_SRCDIR)/,$(notdir $(ALL_BATCH_CMO)))" >> $@ - $(ECHO) "DYN_OLINKFLAGS=$(filter-out $(INCLUDES),$(OLINKFLAGS)) $(foreach d,$(INCLUDES:-I%=%),-I $(FRAMAC_ROOT_SRCDIR)/$(d))" >> $@ - $(ECHO) "DYN_GEN_OPT_LIBS=$(addprefix $(FRAMAC_ROOT_SRCDIR)/,$(GEN_OPT_LIBS))" >> $@ - $(ECHO) "DYN_OPT_LIBS=$(filter-out $(GEN_OPT_LIBS),$(OPT_LIBS))" >> $@ - $(ECHO) "DYN_ALL_BATCH_CMX=$(addprefix $(FRAMAC_ROOT_SRCDIR)/,$(ALL_BATCH_CMX))" >> $@ - $(ECHO) "else" >> $@ $(ECHO) "DYN_BLINKFLAGS=$(filter-out $(INCLUDES),$(BLINKFLAGS)) $(addprefix -I ,$(filter +%,$(INCLUDES)))" >> $@ $(ECHO) "DYN_GEN_BYTE_LIBS=$(addprefix $(FRAMAC_LIBDIR)/,$(notdir $(GEN_BYTE_LIBS)))" >> $@ $(ECHO) "DYN_BYTE_LIBS=$(filter-out $(GEN_BYTE_LIBS),$(BYTE_LIBS))" >> $@ @@ -63,7 +53,6 @@ share/Makefile.kernel: Makefile.generating share/Makefile.config share/Makefile. $(ECHO) "DYN_GEN_OPT_LIBS=$(addprefix $(FRAMAC_LIBDIR)/,$(notdir $(GEN_OPT_LIBS)))" >> $@ $(ECHO) "DYN_OPT_LIBS=$(filter-out $(GEN_OPT_LIBS),$(OPT_LIBS))" >> $@ $(ECHO) "DYN_ALL_BATCH_CMX=$(addprefix $(FRAMAC_LIBDIR)/,$(notdir $(ALL_BATCH_CMX)))" >> $@ - $(ECHO) "endif" >> $@ $(CHMOD_RO) $@ ALL_LIBRARY_NAMES=$(shell ocamlfind query -r -p-format $(LIBRARY_NAMES) $(LIBRARY_NAMES_GUI)) diff --git a/share/Makefile.dynamic b/share/Makefile.dynamic index 5467a7e18ae..fbdd26a5cf8 100644 --- a/share/Makefile.dynamic +++ b/share/Makefile.dynamic @@ -193,8 +193,6 @@ TARGETS_GUI := $(TARGET_GUI_CMI) $(TARGET_GUI_CMO) \ TARGETS_BYTE:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMO) $(TARGET_TOP_CMA) TARGETS_OPT:= $(TARGET_META) $(TARGET_CMI) $(TARGET_TOP_CMX) $(TARGET_TOP_CMXS) -include $(MAKECONFIG_DIR)/Makefile.kernel - byte:: $(TARGETS_BYTE) opt:: $(TARGETS_OPT) gui:: $(TARGETS_GUI) @@ -206,6 +204,8 @@ ifneq ($(FRAMAC_INTERNAL),yes) # Static Linking # ################## +include $(MAKECONFIG_DIR)/Makefile.kernel + $(PLUGIN_DIR)/frama-c-$(PLUGIN_NAME).byte$(EXE): $(TARGET_TOP_CMO) $(PRINT_LINKING) $@ $(OCAMLC) $(PLUGIN_LINK_BFLAGS) $(DYN_BLINKFLAGS) \ -- GitLab