From c90365e560e6d4860ac1d07ba762f844c4803f33 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Tue, 2 Jul 2013 11:24:30 -0600 Subject: [PATCH] another "distro-build" fix --- pkgs/distro-build/config.rkt | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/pkgs/distro-build/config.rkt b/pkgs/distro-build/config.rkt index 9f4a9bb87e..dee5b9a3f5 100644 --- a/pkgs/distro-build/config.rkt +++ b/pkgs/distro-build/config.rkt @@ -10,11 +10,15 @@ ;; and/or `DOC_SEARCH' configuration from the makefile. ;; ;; The site configuration file otherwise describes and configures -;; client machines. Each client is built by running commands via -;; `ssh', where the client's host (and optional port and/or user) -;; indicate the ssh target. Each client machine must be set up with a -;; public-key authenticaion, because a direct `ssh' is expected to -;; work without a password prompt. +;; client machines hierarchically, where configuration options +;; propagate down the hierarchy when they are not overridden more +;; locally. +;; +;; Each client is built by running commands via `ssh', where the +;; client's host (and optional port and/or user) indicate the ssh +;; target. Each client machine must be set up with a public-key +;; authenticaion, because a direct `ssh' is expected to work without a +;; password prompt. ;; ;; On the client machine, all work is performed with a git clone at a ;; specified directory. The directory defaults to "build/plt" (Unix, @@ -232,7 +236,7 @@ extract-options) (module reader syntax/module-reader - distro-build/site) + distro-build/config) (struct site-config (tag options content))