diff options
Diffstat (limited to 'include')
-rw-r--r-- | include/functions.php | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/include/functions.php b/include/functions.php index d6c73343e..8db72f56d 100644 --- a/include/functions.php +++ b/include/functions.php @@ -478,11 +478,6 @@ print "</select>"; } - function getmicrotime() { - list($usec, $sec) = explode(" ",microtime()); - return ((float)$usec + (float)$sec); - } - function print_radio($id, $default, $true_is, $values, $attributes = "") { foreach ($values as $v) { @@ -1864,6 +1859,8 @@ "prev_feed" => __("Open previous feed"), "next_article" => __("Open next article"), "prev_article" => __("Open previous article"), + "next_article_noscroll" => __("Open next article (don't scroll long articles)"), + "prev_article_noscroll" => __("Open previous article (don't scroll long articles)"), "search_dialog" => __("Show search dialog")), __("Article") => array( "toggle_mark" => __("Toggle starred"), @@ -1924,6 +1921,8 @@ "p" => "prev_article", "(38)|up" => "prev_article", "(40)|down" => "next_article", + "^(38)|Ctrl-up" => "prev_article_noscroll", + "^(40)|Ctrl-down" => "next_article_noscroll", "(191)|/" => "search_dialog", // "article" => array( "s" => "toggle_mark", @@ -2796,7 +2795,7 @@ $id = 'AUDIO-' . uniqid(); - $entry .= "<audio id=\"$id\"\" controls> + $entry .= "<audio id=\"$id\"\" controls style='display : none'> <source type=\"$ctype\" src=\"$url\"></source> </audio>"; @@ -3065,7 +3064,7 @@ } function print_checkpoint($n, $s) { - $ts = getmicrotime(); + $ts = microtime(true); echo sprintf("<!-- CP[$n] %.4f seconds -->", $ts - $s); return $ts; } |