<?php
/**
* Check whether the php-armadillo extension is loaded.
*
* @return bool
*/
function is_php_arma_loaded() {
if (!extension_loaded('arma')) {
echo 'skip armadillo extension is not loaded.';
return false;
}
return true;