From 8e65220f3bb05f49438e6eff8b5faa8dac324364 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sat, 10 Jun 2006 21:42:02 +0000 Subject: [PATCH] fixed bug just introduced when adding planet docs ... svn: r3319 --- collects/help/private/gui.ss | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/collects/help/private/gui.ss b/collects/help/private/gui.ss index 3a3f0c8a68..a06e22cbd7 100644 --- a/collects/help/private/gui.ss +++ b/collects/help/private/gui.ss @@ -117,11 +117,6 @@ url] ;; one of the "collects" hosts: - [(and (equal? internal-port (url-port url)) - (is-internal-host? (url-host url))) - url] - - ;; one of the "doc" hosts: [(and (equal? internal-port (url-port url)) (ormap (lambda (host) (equal? host (url-host url))) @@ -165,6 +160,11 @@ url)) ;; Not a manual? Shouldn't happen. url))] + + ;; one of the other internal hosts + [(and (equal? internal-port (url-port url)) + (is-internal-host? (url-host url))) + url] ;; send the url off to another browser [(or (and (string? (url-scheme url))