commit d8eeb4bb8155542decd7bf3b5fd402c0d12302a8
parent b99617cf8639dd64cdc3bc702f782f8c40903961
Author: Paul Steckler <steck@stecksoft.com>
Date: Fri, 27 Sep 2002 20:27:53 +0000
..
original commit: 8cd4fb79757fc7aeb401b3cba15f83f7b1ff6e36
Diffstat:
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/collects/help/help.ss b/collects/help/help.ss
@@ -4,6 +4,7 @@
(lib "cmdline.ss")
"private/server.ss"
"private/browser.ss"
+ "private/start.ss"
"private/plt-browser.ss")
(define launch-browser? #t)
@@ -57,7 +58,10 @@
(hd-cookie->port hd-cookie))))])
(help-desk-browser hd-cookie)
; allow browser startup time
- (sleep 2)))
+ (sleep (add1 browser-timeout))
+ ; starting an external browser may have failed
+ ; so we may have switched to the internal browser
+ (set! internal-browser? (use-plt-browser?))))
(cond
[internal-browser? (void)]