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

Commit: c83b6e4a90fb2fa8f1bba71b7c0bb0cd69966378 Author: Hannes Magnusson <bjori@mongodb.com> Sat, 28 Dec 2013 19:18:33 -0800 Parents: b4553253ce539140accb6f106fb002d140ed9304 Branches: master Link: http://git.php.net/?p=web/php.git;a=commitdiff;h=c83b6e4a90fb2fa8f1bba71b7c0bb0cd69966378 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",