From e813b0f9da13fa40d78f7e0a89bc695d96962381 Mon Sep 17 00:00:00 2001 From: Alexis King Date: Sun, 8 Nov 2015 12:50:44 -0800 Subject: [PATCH] Set the reporting port to the error port by default This is important for the get-javascript command, which outputs the result to stdout. In order for this to be useful, it can be redirected to a file, but if reporting information also goes to stdout, then it ends up in the resulting JavaScript. Switching these messages to stderr prevents that problem. --- whalesong/parameters.rkt | 2 +- whalesong/whalesong-cmd.rkt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/whalesong/parameters.rkt b/whalesong/parameters.rkt index 8df577d..e607941 100644 --- a/whalesong/parameters.rkt +++ b/whalesong/parameters.rkt @@ -88,7 +88,7 @@ (: current-report-port (Parameterof Output-Port)) -(define current-report-port (make-parameter (current-output-port))) +(define current-report-port (make-parameter (current-error-port))) (: current-timing-port (Parameterof Output-Port)) diff --git a/whalesong/whalesong-cmd.rkt b/whalesong/whalesong-cmd.rkt index 623142b..fb1cde3 100644 --- a/whalesong/whalesong-cmd.rkt +++ b/whalesong/whalesong-cmd.rkt @@ -200,7 +200,7 @@ (current-verbose? #t)] [("--debug-show-timings") ("Display debug messages about compilation time.") - (current-timing-port (current-output-port))] + (current-timing-port (current-error-port))] [("--enable-profiling") ("Enable profiling to standard output") (with-profiling? #t)]