[14:06:46] hello, anything I can do better to get https://gerrit.wikimedia.org/r/c/mediawiki/core/+/787858/ backported to REL1_35? [19:28:11] I have suggestion to make so that user CSS and other browser extensions, etc can detect a MediaWiki instance on other servers. [19:29:24] zzo38: nice idea. I might say you can already detect it from this though, by the way: [19:29:27] [19:29:37] when cutting off after MediaWiki [19:40:09] Can it be done in CSS? I know that with what I mention, can make something like "html[application=mediawiki]" in a CSS code [19:53:59] zzo38: You can change CSS on your wiki just by editing wiki pages: https://www.mediawiki.org/wiki/Manual:CSS [19:54:24] zzo38: if you want to change the default CSS for ALL mediawikis then please create a Phabricator ticket for that [20:03:40] Neither is what I am trying to do. Rather, what I intended is to change it on the client side for all MediaWiki instances, for myself only (and other users can do it for themself only, by defining their own CSS), without an account nor including the CSS changes in MediaWiki itself. [20:07:23] you can use a couple of extensions to replace any CSS on any site. like this https://addons.mozilla.org/en-US/firefox/addon/stylish/ and similar [20:07:38] Adding such a attribute would allow this and potentially other extensions to work (although the that you already have might help some things, but I don't know if CSS can make a selector based on this) [20:08:09] mutante: I know that. But you will have to do it specifically for each site, unless there is some selector to select all MediaWiki instances all at once. [20:08:54] (Furthermore, CSS is not necessarily the only thing that might want to do things like this; e.g. you might have extensions for other functions of MediaWiki (and other web apps) too.) [20:09:10] so you do actually want to change the default for all mediawikis? [20:10:43] Yes, but only on the client side. [20:16:43] I don't really understand. You want MediaWiki upstream to change something in CSS so that you can then change it locally. Did i get that right? [20:17:15] so if it requires MW to do something different from what it does now then that would be like a feature request. [21:11:01] zzo38: looks like wikis already have the element tagged with class="mediawiki" [21:11:58] Also, there's a class name for the skin used, which makes more sense when you want to style things [21:23:34] mutante: No. They need not change any CSS upstream; only the HTML change. [21:24:18] Vulpix: OK, that will work, although what I suggestion is for more than only CSS, but also API clients, other extensions, etc. Of course that works but it doesn't seem ideal to me [21:29:13] you have a solution that works *today* for quite a lot of wikis. An ideal solution may take years to be usable, since it needs to be developed, and then the wikis would need to be upgraded [21:33:32] OK [22:09:46] so you said the same thing that it's already in HTML source but then it works