diff options
author | Michael Stahl <mstahl@redhat.com> | 2017-07-27 13:18:11 +0200 |
---|---|---|
committer | Michael Stahl <mstahl@redhat.com> | 2017-07-27 14:42:24 +0200 |
commit | 1176ae51154c2298b44427270754d2ee1562a115 (patch) | |
tree | 8acffc51fb2c1fa9019424adcd913ac6fdb0b5c1 /Makefile.in | |
parent | 81047eaebc0e25ff926bf944c57e082a8727c7f2 (diff) |
Makefile: fix fetching for the build platform
The invocation of make fetch added in commit
fe3fb5ecd3b66e32cc5aa64a2afffa572353740e didn't do anything because
the force-restart didn't actually restart make because it touched
"Makefile" but the make read "$(BUILDDIR)/Makefile", and make isn't
smart enough to notice those are the same.
Change-Id: I85cbcba3bf9c3c7b89d4ee33f772820d19542f4a
Reviewed-on: https://gerrit.libreoffice.org/40482
Tested-by: Jenkins <ci@libreoffice.org>
Reviewed-by: Michael Stahl <mstahl@redhat.com>
Diffstat (limited to 'Makefile.in')
-rw-r--r-- | Makefile.in | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile.in b/Makefile.in index 4b7048438bc4..62adf2bb56b1 100644 --- a/Makefile.in +++ b/Makefile.in @@ -30,8 +30,11 @@ GIT_BUILD := $(if $(wildcard $(SRCDIR)/.git),T) # need updated configuration ifeq (,$(MAKE_RESTARTS)$(if $(GIT_BUILD),,T)$(if $(filter-out help showmodules clean distclean,$(MAKECMDGOALS)),,T)) +# note: this must touch both Makefile and $(BUILDDIR)/Makefile, because make +# may be invoked using either of these paths, and it will restart itself only +# if the updated target is exactly the same path as the Makefile it is using .PHONY : force-restart -Makefile: $(BUILDDIR)/config_host.mk $(BUILDDIR)/config_host_lang.mk force-restart +Makefile $(BUILDDIR)/Makefile: $(BUILDDIR)/config_host.mk $(BUILDDIR)/config_host_lang.mk force-restart @touch $@ # run configure in an environment not polluted by config_host.mk |