From fdb8d72700feceb587cebe0696531b2447467f5c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 13 Jul 2002 17:53:12 +0000
Subject: Change colour but not boldness

---
 html/header.html | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'html')

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>";
-- 
cgit v1.2.3