require_once( "$IP/extensions/HTMLets/HTMLets.php" );

$wgHTMLetsDirectory = "$IP/htmlets";