Last modified: 2013-09-11 22:45:51 UTC

Wikimedia Bugzilla is closed!

Wikimedia migrated from Bugzilla to Phabricator. Bug reports are handled in Wikimedia Phabricator.
This static website is read-only and for historical purposes. It is not possible to log in and except for displaying bug reports and their history, links might be broken. See T51914, the corresponding Phabricator task for complete and up-to-date bug report information.

Bug 49914 - @mediawiki::extension does not let you set default user options


Summary:	@mediawiki::extension does not let you set default user options

Status:	RESOLVED WORKSFORME

Product:	MediaWiki-Vagrant
Classification:	Unclassified
Component:	General (Other open bugs)
Version:	unspecified
Hardware:	All All

Importance:	Unprioritized normal
Target Milestone:	---
Assigned To:	Ori Livneh

URL:
Whiteboard:
Keywords:

Depends on:
Blocks:
	Show dependency tree / graph

Reported:	2013-06-20 22:34 UTC by Yuvi Panda
Modified:	2013-09-11 22:45 UTC (History)
CC List:	1 user (show)

See Also:
Web browser:	---
Mobile Platform:	---
Assignee Huggle Beta Tester:	---

Attachments
Add an attachment (proposed patch, testcase, etc.)

Description Yuvi Panda 2013-06-20 22:34:03 UTC

Useful for extensions such as WikiEditor, to set $wgDefaultUserOptions

Comment 1 Ori Livneh 2013-06-20 22:35:05 UTC

It does; just supply a 'settings' key.

Comment 2 Ori Livneh 2013-07-06 07:16:28 UTC

For example,

    @mediawiki::extension { 'WikiEditor':
        settings => [
            '$wgDefaultUserOptions['favoritecars-black-jetta'] = 1'
        ],
    }

Comment 3 Andre Klapper 2013-09-11 22:45:51 UTC

[mass-moving from Tools>MediaWiki-Vagrant to separate product. See bug 54041. Filter bugmail on this comment.]

Wikimedia Bugzilla is closed!

Search

Personal tools

Navigation

Links