diff --git a/collects/mred/private/misc.ss b/collects/mred/private/misc.ss index 5036f36aef..a41e27aaa4 100644 --- a/collects/mred/private/misc.ss +++ b/collects/mred/private/misc.ss @@ -71,7 +71,12 @@ 'play-sound "not supported by default on this platform" subpath)])))]) - ((if async? (lambda (x) (process x) #t) system) + ((if async? + (lambda (x) + (process/ports + (current-output-port) (current-input-port) (current-error-port) x) + #t) + system) (format cmd (string-append "\"" (regexp-replace* #rx"([$\"\\])"