diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-05-17 17:30:03 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-17 17:30:03 +0200 |
commit | 5b7fc96afb149ad916a9bf5015fe1eb2e0baaa7c (patch) | |
tree | 03ec4c313a1b7f220e37bd924082565a0a4df6a8 /runtime/Makefile | |
parent | 99918e4118e0ea644b20e37a13ceb31d935fdda5 (diff) | |
download | compcert-5b7fc96afb149ad916a9bf5015fe1eb2e0baaa7c.tar.gz compcert-5b7fc96afb149ad916a9bf5015fe1eb2e0baaa7c.zip |
Prepend $(DESTDIR) to the installation target (#169)
Following the gnu Makefile Conventions the variable $(DESTDIR)
should be prepended to all installation commands. This allows
staged installs.
Diffstat (limited to 'runtime/Makefile')
-rw-r--r-- | runtime/Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/runtime/Makefile b/runtime/Makefile index 27ad6e8c..8fe00934 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -70,16 +70,16 @@ clean:: ifeq ($(strip $(HAS_RUNTIME_LIB)),true) install:: - install -d $(LIBDIR) - install -m 0644 $(LIB) $(LIBDIR) + install -d $(DESTDIR)$(LIBDIR) + install -m 0644 $(LIB) $(DESTDIR)$(LIBDIR) else install:: endif ifeq ($(strip $(HAS_STANDARD_HEADERS)),true) install:: - install -d $(LIBDIR)/include - install -m 0644 $(INCLUDES) $(LIBDIR)/include + install -d $(DESTDIR)$(LIBDIR)/include + install -m 0644 $(INCLUDES) $(DESTDIR)$(LIBDIR)/include else install:: endif |