From 7f9c9ee7aec56c615e3a075369f98de791808467 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Sun, 18 Aug 2013 16:30:42 -0600 Subject: [PATCH] distro-build/drive-clients: print time before each command original commit: a961b63a2587727cc79831253658e7b77c0f44e8 --- 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 db349a1..490ec5e 100644 --- a/pkgs/distro-build/drive-clients.rkt +++ b/pkgs/distro-build/drive-clients.rkt @@ -194,6 +194,7 @@ (define (ssh-script host port user kind . cmds) (for/and ([cmd (in-list cmds)]) + (when cmd (display-time)) (or (not cmd) (if (and (equal? host "localhost") (not user)) @@ -366,7 +367,6 @@ ;; ensure a newline at the end: (newline o)))) - (display-time) (begin0 ((case (or (get-opt c '#:platform) (system-type))