wikimedia/mediawiki-extensions-WikiEditor
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/WikiEditor synced 2024-11-24 16:26:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

Merge "Hide MediaWiki's "Editing help" link, as we provide it in the toolbar"

Browse source
This commit is contained in:
jenkins-bot 2013-08-15 18:38:10 +00:00 committed by Gerrit Code Review
parent 589f90ab81 6f8acfaf2b
commit 61bed82f7f
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
modules/ext.wikiEditor.css
View file

@ -2,19 +2,16 @@
* CSS for WikiEditor
*/
/* This ID (#editform) could change in MediaWiki */
form#editform {
margin: 0;
padding: 0;
}
/* These IDs (#wpSummaryLabel and #wpSummary) could change in MediaWiki */
#wpSummary,
#wpSummaryLabel {
margin-bottom: 1em;
}
/* This ID (#wpTextbox1) could change in MediaWiki */
.wikiEditor-ui textarea#wpTextbox1 {
border: none;
padding: 0;
@ -26,3 +23,9 @@ form#editform {
.wikiEditor-ui .wikiEditor-ui-text > textarea#wpTextbox1 {
margin: 0;
}
/* Hide vanilla MediaWiki's "Editing help" link, as we provide it in the toolbar */
.editButtons .editHelp,
.editButtons .mw-editButtons-pipe-separator {
display: none;
}