diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-07-13 17:53:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-07-13 17:53:12 +0000 |
| commit | fdb8d72700feceb587cebe0696531b2447467f5c (patch) | |
| tree | 75ca415bd18fcf855fa7828245e3703b3fd1bbf9 /html | |
| parent | e54b86825f2bf3308ff06973dfc5706aba55355e (diff) | |
Change colour but not boldness
Diffstat (limited to 'html')
| -rw-r--r-- | html/header.html | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/html/header.html b/html/header.html index 46d76d3b..bc166da5 100644 --- a/html/header.html +++ b/html/header.html @@ -1,7 +1,9 @@ <!-- This is the header --> -<table width="600"> +<table width="650"> <tr> <td width="100"> +<!-- FIXME: this used to link to root, not reliable now: neither does / or .. + do the right thing. --> <a href=""> <img src="images/ProofGeneral.jpg" alt="Proof General" align=top width=90 height=119 border=0 > @@ -21,7 +23,7 @@ $urlbits = parse_url($REQUEST_URI); $file = ereg_replace("^(.*/)+","",$urlbits["path"]); $WANTED = ereg_replace(".html","",$file); - print "<table class=\"menubar\"><tr>\n"; + print "<table width=\"80%\" class=\"menubar\"><tr>\n"; $links_arr = array( "Home" => "main", "Features" => "features", @@ -46,7 +48,7 @@ for (reset($links_arr); $name = key($links_arr); next($links_arr)) { print $separator; if ($WANTED == $links_arr[$name]) { - print "<b>" . $name . "</b>"; + print "<font color=\"white\">" . $name . "</font></b>"; } else { print "<a href=\"$links_arr[$name]\">$name</a>"; |