summaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 7 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 9b888e7cca..8046e36e14 100644
--- a/Makefile
+++ b/Makefile
@@ -129,9 +129,15 @@ endif
@echo "===--- building final phase"
$(MAKE) --no-print-directory -f ghc.mk phase=final $@
+# if BINARY_DIST_DIR is not set, assume we want the old
+# behaviour of placing the binary dist into the current
+# directory. Provide BINARY_DIST_DIR to put the final
+# binary distribution elsewhere.
+BINARY_DIST_DIR ?= .
+
.PHONY: binary-dist
binary-dist: binary-dist-prep
- mv bindistprep/*.tar.$(TAR_COMP_EXT) .
+ mv bindistprep/*.tar.$(TAR_COMP_EXT) "$(BINARY_DIST_DIR)"
.PHONY: binary-dist-prep
binary-dist-prep: