From 8754348eafb18af10328e87629df2398f43f0f1f Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Fri, 11 Oct 2002 19:10:46 +0000 Subject: [PATCH] . original commit: 77e5a9212e4e76382f0cadb82cf61e743927947b --- collects/help/help.ss | 1 + 1 file changed, 1 insertion(+) diff --git a/collects/help/help.ss b/collects/help/help.ss index f1990406..c0921e47 100644 --- a/collects/help/help.ss +++ b/collects/help/help.ss @@ -35,6 +35,7 @@ (set! port port-val)))])) (define hd-cookie (start-help-server port external-connections?)) + (unless hd-cookie (exit)) (define help-desk-port (hd-cookie->port hd-cookie)) (define internal-browser? (use-plt-browser?))