mirror of
https://github.com/sbrl/Pepperminty-Wiki.git
synced 2024-11-25 17:23:00 +00:00
Add page index parse time header
This commit is contained in:
parent
bab0f67da0
commit
8fc527fc07
2 changed files with 4 additions and 0 deletions
|
@ -652,7 +652,9 @@ if(!file_exists("./pageindex.json"))
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
$pageindex_read_start = microtime(true);
|
||||||
$pageindex = json_decode(file_get_contents("./pageindex.json"));
|
$pageindex = json_decode(file_get_contents("./pageindex.json"));
|
||||||
|
header("x-pageindex-decode-time: " . round(microtime(true) - $pageindex_read_start, 6) . "ms");
|
||||||
}
|
}
|
||||||
|
|
||||||
// Work around an Opera + Syntaxtic bug where there is no margin at the left hand side if there isn't a query string when accessing a .php file
|
// Work around an Opera + Syntaxtic bug where there is no margin at the left hand side if there isn't a query string when accessing a .php file
|
||||||
|
|
2
core.php
2
core.php
|
@ -343,7 +343,9 @@ if(!file_exists("./pageindex.json"))
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
$pageindex_read_start = microtime(true);
|
||||||
$pageindex = json_decode(file_get_contents("./pageindex.json"));
|
$pageindex = json_decode(file_get_contents("./pageindex.json"));
|
||||||
|
header("x-pageindex-decode-time: " . round(microtime(true) - $pageindex_read_start, 6) . "ms");
|
||||||
}
|
}
|
||||||
|
|
||||||
// Work around an Opera + Syntaxtic bug where there is no margin at the left hand side if there isn't a query string when accessing a .php file
|
// Work around an Opera + Syntaxtic bug where there is no margin at the left hand side if there isn't a query string when accessing a .php file
|
||||||
|
|
Loading…
Reference in a new issue