wikimedia/mediawiki-extensions-Gadgets
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/Gadgets synced 2024-12-22 19:52:39 +00:00
Code Issues Packages Projects Releases Wiki Activity
1566 commits 15 branches 25 tags 23 MiB
Commit graph

6 commits

Author SHA1 Message Date
Kunal Mehta e99e181303 Add phan configuration 
Depends-On: I09a0c0a786b687997e61344847f8af08b20cebf2
Change-Id: I9500232fb524e884d6cb15f2bdda10835df35ad4
 2018-02-26 12:57:40 -08:00
Umherirrender 5bbb1045fe Expand .gitignore for more editors 
List is from mediawiki/core

Change-Id: I65afe486373f81ed8fa2503e4b772387a9002458
 2016-11-13 12:57:04 +01:00
paladox 11a683dd07 Update Jenkins tests 
Run jshint through npm instead.

Also add composer.json to run phplint and in future run the php code sniffer.

Signed-off-by: Antoine Musso <hashar@free.fr>
Change-Id: I1797ac2bce1936ed75da76618f28fc239b60001b
 2015-11-19 15:19:35 +01:00
Kunal Mehta a6b1a9c5e6 build: Configure banana-checker and jsonlint 
Change-Id: If8853a6c49398d5769f2b20bd5d81c83f25f0b74
 2015-06-17 19:52:25 +01:00
Siebrand Mazeland bf416b175a Maintenance for Gadgets extension. 
* Use Message class.
* Redice globals usage.
* Update .gitignore.

Change-Id: I087c8209b1a7ccf63171a2c14c8809eed90a297b
 2012-08-17 11:28:09 +02:00
Reedy 7bd094ff68 Add .gitignore 
Change-Id: I4a19650ef68655cd8d6238536849a6082c353a96
 2012-05-21 01:36:24 +01:00