From bd7aa7923a25d16207842f9f3d6b773c2fc6fa58 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 28 Sep 2000 15:01:50 +0000
Subject: Renamed file

---
 html/header.phtml | 60 -------------------------------------------------------
 1 file changed, 60 deletions(-)
 delete mode 100644 html/header.phtml

(limited to 'html/header.phtml')

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