|
From: Dirk M. <mu...@kd...> - 2003-12-02 20:32:11
|
CVS commit by mueller: customize page title M +1 -0 feedback.html 1.5 M +8 -3 header.inc 1.8 --- devel-home/valgrind/feedback.html #1.4:1.5 @@ -1,3 +1,4 @@ <?php + $page_title = "Sending Feedback"; include "header.inc" ?> --- devel-home/valgrind/header.inc #1.7:1.8 @@ -1,7 +1,12 @@ -<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" -"http://www.w3.org/TR/html4/loose.dtd"> +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <html> <head> -<title>Valgrind</title> +<?php + if (isset($page_title)) + $title = "Valgrind - $page_title"; + else + $title = "Valgrind"; +?> +<title><?php print $title; ?></title> <link rel="stylesheet" type="text/css" href="style.css"> </head> |