mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/Echo
synced 2024-11-13 17:57:21 +00:00
71c7e02858
* Port Flow Makefile to Echo * Move resources to Resources.php Change-Id: I75e96cc1e51a7768600ffc083550fc94ea9d1e6c
30 lines
665 B
PHP
Executable file
30 lines
665 B
PHP
Executable file
<?php
|
|
if ( sizeof( $argv ) < 3 ) {
|
|
print "Call with 2 arguments: the path to the load url and the file to output to";
|
|
exit();
|
|
}
|
|
$loadUrl = $argv[1];
|
|
$outputFile = $argv[2];
|
|
|
|
define( 'MEDIAWIKI', true );
|
|
const NS_MAIN = 0;
|
|
$wgVersion = 1.23;
|
|
$wgSpecialPages = array();
|
|
$wgResourceModules = array();
|
|
|
|
include "Resources.php";
|
|
|
|
$query = array();
|
|
$blacklist = array(
|
|
);
|
|
foreach( $wgResourceModules as $moduleName => $def ) {
|
|
if ( !in_array( $moduleName, $blacklist ) ) {
|
|
$query[] = $moduleName;
|
|
}
|
|
}
|
|
|
|
$url = $loadUrl . '?only=styles&skin=vector&modules=' . implode( $query, '|' );
|
|
echo $url;
|
|
$css = file_get_contents($url);
|
|
file_put_contents( $outputFile, $css );
|