<?php
/*
 * InitExtEvent:
 * Get extensions to load themselves
 */
class InitExtEvent extends Event {
	public function InitExtEvent() {
	}
}
?>