If the page doesn't exist and the user can't create it, omit the "edit"/"view source"
[mediawiki.git] / StartProfiler.php
blob3fcf69e6e58bb389f62574f4d6d130164de7c231
1 <?php
3 require_once( dirname(__FILE__).'/includes/ProfilerStub.php' );
5 /**
6 * To use a profiler, delete the line above and add something like this:
8 * require_once( dirname(__FILE__).'/includes/Profiler.php' );
9 * $wgProfiler = new Profiler;
11 * Or for a sampling profiler:
12 * if ( !mt_rand( 0, 100 ) ) {
13 * require_once( dirname(__FILE__).'/includes/Profiler.php' );
14 * $wgProfiler = new Profiler;
15 * } else {
16 * require_once( dirname(__FILE__).'/includes/ProfilerStub.php' );
17 * }
19 * Configuration of the profiler output can be done in LocalSettings.php