From 7f68d463c7e8af3994b21cd32b0926e051108e38 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Sun, 5 Jan 2014 18:39:21 -0700 Subject: [PATCH] make server: fix config setup for pkg build When the server installs packages from source, it needs configuration entry that points documentation indirections to the right place. A relevant "config.rktd" is written, but to the wrong place, so that it wasn't being used. Merge to v6.0 (pending review) (cherry picked from commit 9de2aff3f3c0842a1eb14efa5d0a88dc161de0b7) --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 131ee5fbd8..73be153dc9 100644 --- a/Makefile +++ b/Makefile @@ -322,7 +322,7 @@ fresh-user: rm -rf build/user set-config: - $(RACKET) -l distro-build/set-config racket/etc/config.rktd $(CONFIG_MODE_q) "$(DOC_SEARCH)" "" "" "" + $(RACKET) -l distro-build/set-config build/user/config/config.rktd $(CONFIG_MODE_q) "$(DOC_SEARCH)" "" "" "" # Install packages from the source copies in this directory. The # packages are installed in user scope, but we set the add-on