diff options
Diffstat (limited to 'tools/klee-stats/Makefile')
| -rw-r--r-- | tools/klee-stats/Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/klee-stats/Makefile b/tools/klee-stats/Makefile index 89578b12..219d41da 100644 --- a/tools/klee-stats/Makefile +++ b/tools/klee-stats/Makefile @@ -36,11 +36,11 @@ install-local:: uninstall-local:: $(Echo) Uninstall circumvented with NO_INSTALL else -DestTool = $(PROJ_bindir)/$(TOOLSCRIPTNAME) +DestTool = $(DESTDIR)$(PROJ_bindir)/$(TOOLSCRIPTNAME) install-local:: $(DestTool) -$(DestTool): $(ToolBuildPath) $(PROJ_bindir) +$(DestTool): $(ToolBuildPath) $(DESTDIR)$(PROJ_bindir) $(Echo) Installing $(BuildMode) $(DestTool) $(Verb) $(ProgInstall) $(ToolBuildPath) $(DestTool) |