mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/WikiEditor
synced 2024-11-15 03:35:58 +00:00
12e5de632e
We had some crazy stuff here with negative margins, border boxes and what not. There were some problems with IE versions, zooming in and out in pages and with the side by side preview. This should take care of those. Mostly it moves the borders inside the elements that are 100%. This was also required because of the side-by-side preview which was using a dirty trick to hide the border at the top Bug: 26828 Change-Id: I3c3466fac53df3e79de6f12f404005e55409fa7c
27 lines
409 B
CSS
27 lines
409 B
CSS
/**
|
|
* CSS for WikiEditor
|
|
*/
|
|
|
|
form#editform {
|
|
margin: 0;
|
|
padding: 0;
|
|
}
|
|
|
|
#wpSummary,
|
|
#wpSummaryLabel {
|
|
margin-bottom: 1em;
|
|
}
|
|
|
|
.wikiEditor-ui textarea#wpTextbox1 {
|
|
border: none;
|
|
padding: 0;
|
|
line-height: 1.5em;
|
|
resize: vertical;
|
|
}
|
|
|
|
/* Hide vanilla MediaWiki's "Editing help" link, as we provide it in the toolbar */
|
|
.editButtons .editHelp,
|
|
.editButtons .mw-editButtons-pipe-separator {
|
|
display: none;
|
|
}
|