// If you see this page, your HTTP server is not correctly // configured for 'JavaScript.' // Please press 'BACK' and everything might carry on as normal. agent = navigator.userAgent browserVer = 2 if (agent.indexOf("a/3",6) == -1) { browserVer = 2 } else { browserVer = 1 } if (browserVer == 1) { Active = new Image(26,14); Active.src = "/C_ref/GRAPHICS/redball.gif" NotActive = new Image(26,14); NotActive.src = "/C_ref/GRAPHICS/whiteball.gif" } // ................................................................... function Blob(Href, Name, Str) { Text = "\"o\""; Text += "" + Str + ""; document.write(Text); } // ................................................................... function HiLite(imgDocID, NewImage) { if (browserVer == 1) { document.images[imgDocID].src = eval(NewImage + ".src") } } // ................................................................... // This is executed at the top og each page. function top() { document.write(""); } // ................................................................... // This is executed at the bottom of all HTML pages. function tail(CreateDate, Level) { // ... This stops a JavaScript error if 'Level' is not provided // ... in the call. Level += "x"; // ... 'Level' is not provided. Use default values. if (Level == "undefinedx") { href = "http:/C_ref/"; Address = "http:/C_ref/C/"; Level = "0x"; } // ... 'Level' has been provided. if ("1x" == Level) { href = "../"; Address = ""; } if ("2x" == Level) { href = "../../"; Address = "../"; } document.write("

"); document.write("


"); document.write("

"); document.write("

"); document.write(""); document.write(""); document.write(""); document.write(""); document.write("
"); document.write("Top"); document.write(""); document.write("Master Index"); document.write(""); document.write("C Keywords"); document.write(""); document.write("Functions"); document.write("
"); document.write("
"); document.write("

"); document.write("


"); document.write("
Martin Leslie"); document.write("
Creation Date: "); document.write(CreateDate); document.write("
Last Modification: "); document.write(document.lastModified); document.write("

"); }