diff --git a/collects/scribble/scribble-common.js b/collects/scribble/scribble-common.js index 507f914f..636aee43 100644 --- a/collects/scribble/scribble-common.js +++ b/collects/scribble/scribble-common.js @@ -1,6 +1,6 @@ // Common functionality for PLT documentation pages -function GetCookie(key) { +function GetCookie(key, def) { if (document.cookie.length <= 0) return null; var cookiestrs = document.cookie.split(/; */); for (var i in cookiestrs) { @@ -9,7 +9,7 @@ function GetCookie(key) { if (eql >= 0 && cur.substring(0,eql) == key) return unescape(cur.substring(eql+1)); } - return null; + return def; } function SetCookie(key, val) { @@ -28,7 +28,7 @@ function SetPLTRoot(ver, relative) { // adding index.html works because of the above function GotoPLTRoot(ver, relative) { - var u = GetCookie("PLT_Root."+ver); + var u = GetCookie("PLT_Root."+ver, null); if (u == null) return true; // no cookie: use plain up link // the relative path is optional, default goes to the toplevel start page if (!relative) relative = "index.html"; @@ -47,7 +47,7 @@ function NormalizePath(path) { function DoSearchKey(event, field, ver) { var val = field.value; if (event && event.keyCode == 13 && val.indexOf("...search...") < 0) { - var u = GetCookie("PLT_Root."+ver); + var u = GetCookie("PLT_Root."+ver, null); if (u == null) u = "../"; // default: go up location = u + "search/index.html" + "?q=" + escape(val); return false;