[00:01:53] yeah, no error log whatsoever, only happens when debugging [00:02:16] some sort of xdebug bug i suppose, although the line it dies on looks really harmless [00:02:18] * rdwrer has image of PHP instances spontaneously combusting [00:19:48] ooh this is fun [00:20:27] if a preference defaults to true, you can never change it [00:21:10] i wonder how this did not come out earlier, this cannot be the first preference that defaults to true [00:23:03] What, that's insane [00:23:14] it only happens if the preference does not have a key in $wgDefaultUserOptions [00:23:27] that should be normal, though, shouldn't it? [00:23:45] there only around 50 keys there, we have way more prefs than that [00:23:55] No, I think all prefs are supposed to be in that array [00:24:09] err actually, I can't imagine gadgets are in it [00:24:43] putting an extension pref in a core file would be pretty strange [00:25:17] Well extensions can modify the array later [00:25:59] is there a tutorial on how to add a pref? maybe we are missing a step [00:26:16] What, documentation, in mediawiki! [00:26:20] i looked at some examples but they only call GetPreferences [00:26:35] which MediaViewer does [00:26:51] and it does not end up in $whDefaultUserOptions [00:26:57] Most extensions I've looked at add $wgDefaultUserOptions['pref-name-here'] = false; (or true, etc), to the ExtensionName.php file [00:27:10] e.g. UploadWizard [00:27:43] One's that dynamically add preferences (Gadgets) seem to use UserGetDefaultOptions hook [00:35:37] true, although it seems to only do that for about half the preferences [00:35:46] anyway, still feels like a bug to me [00:36:03] or there should be much clearer documentation on this [00:38:01] There should be clearer documentation on pretty much everything [01:20:29] (03CR) 10Gergő Tisza: "Does not work because of bug 62946." [extensions/MultimediaViewer] - 10https://gerrit.wikimedia.org/r/119981 (owner: 10MarkTraceur) [01:37:20] (03PS3) 10Gergő Tisza: Add user preference for non-beta disabling [extensions/MultimediaViewer] - 10https://gerrit.wikimedia.org/r/119981 (owner: 10MarkTraceur) [01:39:01] bawolff: do you know how false preferences are stored in the DB? [01:40:10] If a preference has its default value, its not stored in the db [01:40:21] Otherwise its in the user_options table [01:41:16] yes, i mean, should it be '' or '0' or 'false' or what? [01:42:47] In my local db, I see a lot of '' [01:43:04] i got to the point where something is added to the db but in effect the preference is still not saved [01:43:09] Which is probably boolean false cast to a string [01:43:25] i was suspicious of the '' but that's all right then [01:44:11] kind of sad that adding a new checkbox to an extension is a one-day effort [01:47:11] (03CR) 10Gergő Tisza: "This works around bug 62946, but saving the preference still does not work. It is saved in the database with the correct value, but read b" [extensions/MultimediaViewer] - 10https://gerrit.wikimedia.org/r/119981 (owner: 10MarkTraceur) [01:56:15] (03CR) 10Brian Wolff: Add user preference for non-beta disabling (031 comment) [extensions/MultimediaViewer] - 10https://gerrit.wikimedia.org/r/119981 (owner: 10MarkTraceur) [01:58:11] tgr: In core, default checked toggles seem to use a numeric 1 as the entry in $wgDefaultUserOptions, and have no 'default' key in the array describing the preference. Perhaps try doing that [02:02:36] that helped, thanks! [02:33:34] (03PS1) 10Brian Wolff: Set X-Content-Duration header on ogg transcodes. [extensions/TimedMediaHandler] - 10https://gerrit.wikimedia.org/r/120185 [09:41:41] (03CR) 10Siebrand: [C: 031] "i18n/L10n reviewed." [extensions/MultimediaViewer] - 10https://gerrit.wikimedia.org/r/119981 (owner: 10MarkTraceur)