Re: perf tools man pages on the web

[Arnaldo Carvalho de Melo]

Em Wed, Aug 17, 2022 at 06:02:25AM -0700, Ian Rogers escreveu:
> On Wed, Aug 17, 2022 at 1:55 AM Adrian Hunter <adrian.hunter@xxxxxxxxx> wrote:
> > Speaking of the wiki, anyone know how to change the
> > "Set $wgLogo to the URL path to your own logo image." image?
 
> +1000
 
> Someone at RedHat knows :-)

Documentation is at the Media Wiki site, admin up to a point was John Kacur,
John?

https://www.mediawiki.org/wiki/Manual:FAQ#Changing_the_interface>

--------------------- 8< ----------------------------------

How do I change the logo?

The logo that appears in the top left of each page is determined by the $wgLogo configuration line in the LocalSettings.php file.

There are two ways to change the logo:

    Upload a picture to your wiki using the normal file uploading interface. This allows the logo to be replaced easily, so you may want to protect the page if you use this method.

        Then add the $wgLogo line to LocalSettings.php, for example:

        $wgLogo = "{$wgUploadPath}/6/62/mylogo.png";

    Upload an image to your server by other means (such as FTP).

        Add the $wgLogo line to LocalSettings.php, for example:

        $wgLogo = "{$wgScriptPath}/mylogo.jpg";

        (In this example, the image is in the same folder as the LocalSettings.php file.)

If you want to change the logo in only specific pages, override #p-logo
css's background-image property or use third party extension like
Extension:LogoFunctions.  Caution! Caution: 	Do not simply overwrite
the default logo installed with MediaWiki (/resources/assets/wiki.png);
this file will be overwritten when you upgrade.  A good size for a
square logo is 135x135px or 150x150px, but the logo need not be square,
especially if it contains text below an image. The maximum logo size in
Vector is ~160x160px, while MonoBook's is ~155x155px. A logo that is too
large will be cut off.

--------------------- 8< ----------------------------------

- Arnaldo