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)
This commit is contained in:
Matthew Flatt 2014-01-05 18:39:21 -07:00
parent 20cec1d43f
commit 9de2aff3f3

View File

@ -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