+/**
+ * @param {boolean} param_enable_sound
+ */
+var set_sound = function(param_enable_sound) {
+ enable_sound = param_enable_sound;
+ if (enable_sound) {
+ $("#soundon").html("<strong>On</strong>");
+ $("#soundoff").html("<a href=\"javascript:set_sound(false)\">Off</a>");
+
+ // Seemingly at least Firefox prefers MP3 over Opus; tell it otherwise,
+ // and also preload the file since the user has selected audio.
+ var ding = document.getElementById('ding');
+ if (ding && ding.canPlayType && ding.canPlayType('audio/ogg; codecs="opus"') === 'probably') {
+ ding.src = 'ding.opus';
+ ding.load();
+ }
+ } else {
+ $("#soundon").html("<a href=\"javascript:set_sound(true)\">On</a>");
+ $("#soundoff").html("<strong>Off</strong>");
+ }
+ if (supports_html5_storage()) {
+ localStorage['enable_sound'] = enable_sound ? 1 : 0;
+ }
+}
+window['set_sound'] = set_sound;
+