com web/php: Relax a tad on the massive doc page caching :): include/shared-manual.inc

Commit: 344352530401219533a0e20e2a994da9639175a7 Author: Hannes Magnusson <bjori@mongodb.com> Sat, 28 Dec 2013 19:18:33 -0800 Parents: 804fb83085688a098878d38653cb9c09987afec7 Branches: master Link: http://git.php.net/?p=web/php.git;a=commitdiff;h=344352530401219533a0e20e2a994da9639175a7 Log: Relax a tad on the massive doc page caching :) Changed paths: M include/shared-manual.inc Diff: diff --git a/include/shared-manual.inc b/include/shared-manual.inc index f253ae5..5916fa3 100644 --- a/include/shared-manual.inc +++ b/include/shared-manual.inc @@ -372,8 +372,13 @@ function manual_setup($setup) { $base = "manual/" . $setup["head"][1] . "/"; $_SERVER["BASE_PAGE"] = "/" . $base . $setup["this"][0]; - $f = $_SERVER["DOCUMENT_ROOT"] . $_SERVER["BASE_PAGE"]; - $lastmod = max(filemtime($f), $lastusernote); + $timestamps = array( + filemtime($_SERVER["DOCUMENT_ROOT"] . $_SERVER["BASE_PAGE"]), + filemtime($_SERVER["DOCUMENT_ROOT"] . "/include/prepend.inc"), + filemtime($_SERVER["DOCUMENT_ROOT"] . "/styles/theme-base.css"), + $lastusernote, + ); + $lastmod = max($timestamps); $config = array( "current" => "docs",