diff options
Diffstat (limited to 'html/header.phtml')
| -rw-r--r-- | html/header.phtml | 60 |
1 files changed, 0 insertions, 60 deletions
diff --git a/html/header.phtml b/html/header.phtml deleted file mode 100644 index e5100744..00000000 --- a/html/header.phtml +++ /dev/null @@ -1,60 +0,0 @@ -<!-- This is the header --> -<table width="550"> -<tr> -<td width="190"> -<a href="index.phtml"> -<img src="images/ProofGeneral.jpg" alt="Proof General" align=top - width=180 height=238 border=0 > -</a> -</td> -<td> - <center> - <img src="images/pg-text.gif" alt="Proof General" width=175 height=76> - <h1>Organize your proofs!</h1> -<?php - /* Header link generator. David Aspinall, June 1999. - * Based orginially on navbar.php3 by Douglas Campbell - * Look for $WANTED in array. If not found, use default of "Home" - * and fix $WANTED. Hrefs are given by page parameter to current doc. - */ - $separator='<td><img src="images/bullethole.gif" width=15 height=15 align="top" alt=".">'; - $WANTED=$HTTP_GET_VARS["page"]; - print "<table><tr>\n"; - $links_arr = array( - "Home" => "main", - "Features" => "features", - "Download" => "download", - "News" => "news", - "Screenshots" => "screenshot", - "Documentation" => "doc", - "Development" => "devel", - "About" => "about", - "Links" => "links" - ); - $DEFAULT = $links_arr["Home"]; - $wanted_okay = 0; - for (reset($links_arr); $name = key($links_arr); next($links_arr)) { - if ($WANTED == $links_arr[$name]) { - $wanted_okay = 1; - } - }; - if (! $wanted_okay) { - $WANTED = "main"; - }; - for (reset($links_arr); $name = key($links_arr); next($links_arr)) { - print $separator; - if ($WANTED == $links_arr[$name]) { - print "<b>" . $name . "</b>"; - } - else { - link_root($links_arr[$name],$name); - } - print " </td>\n"; - if ($name=="Download" || $name=="Documentation") print "</tr>\n<tr>"; - } - print "</tr></table>\n"; -?> -</center> -</td></tr> -</table> -<!-- End of header -->
\ No newline at end of file |