mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/WikiEditor
synced 2024-11-28 02:00:34 +00:00
e7a0484eb5
* Fixed by casting to a String before doing the round-trip check
* While at it, improve user interface to make it harder to make mistakes
and easier to do it "right". By making it an HTML5 "number" input specifically,
and building in min/max settings into the UI.
Old browsers fallback to a plain text input (like it was before).
Most browsers implement this number input by allowing the use of the scroll wheel
and the up/down arrows to adjust the numbers, and not allowing non-numbers or numbers
outside the allowed range.
* Follows-up
|
||
|---|---|---|
| modules | ||
| tests/selenium | ||
| .gitignore | ||
| .gitreview | ||
| .jshintignore | ||
| .jshintrc | ||
| README | ||
| WikiEditor.hooks.php | ||
| WikiEditor.i18n.php | ||
| WikiEditor.php | ||
# WikiEditor provides enhancements to the MediaWiki edit page # This extension requires MediaWiki 1.17+ because it makes use of ResourceLoader. # Example LocalSettings.php additions require_once( "$IP/extensions/WikiEditor/WikiEditor.php" ); # Before configuring this extension, see WikiEditor.php and become familiar with the initial state and structure of the # $wgWikiEditorFeatures configuration variable. Essentially it's an array of arrays, keyed by feature name, each # containing global and user keys with boolean values. "global" indicates that it should be turned on for everyone # always, while user indicates that users should be allowed to turn it on or off in their user preferences. # To enable a preference by default but still allow users to disable it in preferences, use something like... $wgDefaultUserOptions['usebetatoolbar'] = 1; $wgDefaultUserOptions['usebetatoolbar-cgd'] = 1;