From d5bffaf5a35abc594016e39ad9c728c0747d152d Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Sat, 29 Jun 2013 10:11:56 -0600 Subject: [PATCH] distro-build/drive-clients: allow shared `#:host' spec original commit: 35075bf45e798dd925f36050138d1080110ad820 --- pkgs/distro-build/drive-clients.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pkgs/distro-build/drive-clients.rkt b/pkgs/distro-build/drive-clients.rkt index d64b311..0c56313 100644 --- a/pkgs/distro-build/drive-clients.rkt +++ b/pkgs/distro-build/drive-clients.rkt @@ -132,6 +132,7 @@ [(#:dist-dir) (simple-string? val)] [(#:max-vm) (real? val)] [(#:server) (simple-string? val)] + [(#:host) (simple-string? val)] [(#:user) (simple-string? val)] [(#:port) (and (exact-integer? val) (<= 1 val 65535))] [(#:dir) (string? val)] @@ -147,7 +148,6 @@ (define (check-machine-keyword kw val) (case kw [(#:name) (string? val)] - [(#:host) (simple-string? val)] [else (check-group-keyword kw val)])) (define (check-config config)