From b9caaa8e4b66817dbc66d0e79b567b3285869fea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 7 Feb 2004 19:31:13 +0000
Subject: Deleted file

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

(limited to 'html/header.html')

diff --git a/html/header.html b/html/header.html
deleted file mode 100644
index b335ac24..00000000
--- a/html/header.html
+++ /dev/null
@@ -1,61 +0,0 @@
-<!-- This is the header -->
-<table width="650">
-<tr>
-<td width="100">
-<a href=".">
-<img src="images/ProofGeneral.jpg" alt="Proof General" width=90 height=119 border=0>
-</a>
-</td>
-<td>
-<center>
-  <img src="images/pg-text.gif" alt="Proof General" width=170 height=17 border=0>
-  <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 width=10em><img align=left src="images/bullethole.gif" width=15 height=15 alt=".">&nbsp;';
-    $urlbits = parse_url($REQUEST_URI);
-    $file = ereg_replace("^(.*/)+","",$urlbits["path"]);
-    $WANTED = ereg_replace(".html","",$file);
-    print "<table  width=\"80%\" class=\"menubar\"><tr align=\"left\">\n"; 
-    $links_arr  =  array(
-          "Home"          =>  "main", 
-	  "Features"	  =>  "features",
-	  "Download"      =>  "download",
-          "Documentation" =>  "doc",
-
-          "News"          =>  "news", 
-          "Screenshots"   =>  "screenshot",
-	  "Development"	  =>  "devel",
-	  "About"	  =>  "about"
-    );
-    $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 "<font color=\"white\">" . $name . "</font>";
-	  }
-	else {
-          print "<a href=\"$links_arr[$name]\">$name</a>";
-	}
-        print " </td>\n";
-        if ($name=="Documentation") print "</tr >\n<tr>";
-    }
-    print "</tr></table>\n"; 
-?>
-</td></tr>
-</table>
-</center>
-<!-- End of header -->
\ No newline at end of file
-- 
cgit v1.2.3