// Check if given extension is active
function EXT_IS_ACTIVE ($ext_name) {
// Extensions are all inactive during installation
// Check if given extension is active
function EXT_IS_ACTIVE ($ext_name) {
// Extensions are all inactive during installation