wikimedia/mediawiki-extensions-DiscussionTools
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/DiscussionTools synced 2024-11-28 18:21:50 +00:00
Code Issues Packages Projects Releases Wiki Activity
488 commits 11 branches 4 tags 128 MiB
Commit graph

7 commits

Author SHA1 Message Date
Ed Sanders e9f2bb80d1 Call the linter API directly if installed 
If the Linter extension is not installed, just allow the page
to be edited.

Bug: T253799
Change-Id: Id3e4c9c2d48aa7ab0b270f41d33ec19184af9a48
 2020-06-04 09:46:07 -05:00
Bartosz Dziewoński 5675eea4d0 Avoid deprecated User::getOption() 
Change-Id: Iad32c3e63116c54c47cd3aa2aaf142c5dd5404c5
 2020-05-21 13:12:49 +00:00
Ed Sanders 5feb69612f Create a user preference to store visual/source mode 
Bug: T250523
Depends-On: I5b3b47feeeca2085fcd283d55d7e9ceafa73be70
Change-Id: I18f5d38f9d694b12e5f983be7b3b165f135a890d
 2020-05-20 22:16:19 +01:00
jenkins-bot 21a892d5e7 Merge "Follow-up b78fb3f4: Make sure we're using a MW User" 2020-05-15 20:38:42 +00:00
James D. Forrester d775f30791 Follow-up b78fb3f4: Make sure we're using a MW User 
Change-Id: Iafd4d3b17a873c0702a64e063a1d0d7e19cf572b
 2020-05-15 13:18:06 -07:00
Ed Sanders e6e0b1ead9 PHP: Add missing typehints 
Change-Id: I5639f8cbdae9aaa9cfa06136e19cc94f9fad10ea
 2020-05-15 22:04:47 +02:00
Ed Sanders b78fb3f4c1 Move all PHP to the MediaWiki\Extension\DiscussionTools namespace 
Change-Id: I654ebb3e646a6d8d62f7bd14d48805e39f836d7e
 2020-05-15 21:57:13 +02:00
Renamed from includes/DiscussionToolsHooks.php (Browse further)