2012-11-30 18:33:32 +01:00
|
|
|
var util = (function () {
|
|
|
|
|
|
|
|
var exports = {};
|
|
|
|
|
|
|
|
// From MDN: https://developer.mozilla.org/en-US/docs/JavaScript/Reference/Global_Objects/Math/random
|
|
|
|
exports.random_int = function random_int(min, max) {
|
|
|
|
return Math.floor(Math.random() * (max - min + 1)) + min;
|
|
|
|
};
|
|
|
|
|
2012-12-17 22:55:10 +01:00
|
|
|
// We need to reset the favicon after changing the
|
|
|
|
// window.location.hash or Firefox will drop the favicon. See
|
|
|
|
// https://bugzilla.mozilla.org/show_bug.cgi?id=519028
|
|
|
|
exports.reset_favicon = function () {
|
|
|
|
$('link[rel="shortcut icon"]').detach().appendTo('head');
|
|
|
|
};
|
|
|
|
|
2012-11-30 18:33:32 +01:00
|
|
|
return exports;
|
|
|
|
}());
|