From b47b1682f1ed07f848f966620decf83e06e31f56 Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Wed, 28 May 2008 00:20:58 +0000 Subject: [PATCH] toc links on main pages go to user pages where needed svn: r9993 original commit: 9b0492e320cf761bd2831fabd64c12e723967092 --- collects/scribble/manual.ss | 4 ++-- collects/scribble/scribble-common.js | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/collects/scribble/manual.ss b/collects/scribble/manual.ss index 0a2468a4..691f791d 100644 --- a/collects/scribble/manual.ss +++ b/collects/scribble/manual.ss @@ -335,8 +335,8 @@ (define (procedure . str) (make-element "schemeresult" `("#"))) -(define (link url - #:underline? [underline? #t] +(define (link url + #:underline? [underline? #t] #:style [style (if underline? #f "plainlink")] . str) (make-element (make-target-url url style) diff --git a/collects/scribble/scribble-common.js b/collects/scribble/scribble-common.js index c1aab351..1aef1c0d 100644 --- a/collects/scribble/scribble-common.js +++ b/collects/scribble/scribble-common.js @@ -27,10 +27,12 @@ function SetPLTRoot(ver, relative) { } // adding index.html works because of the above -function GotoPLTRoot(ver) { +function GotoPLTRoot(ver, relative) { var u = GetCookie("PLT_Root."+ver); if (u == null) return true; // no cookie: use plain up link - location = u + "index.html"; + // the relative path is optional, default goes to the toplevel start page + if (!relative) relative = "index.html"; + location = u + relative; return false; }