}
}
+/// sometimes default PHP settings are borked on shared hosting servers, I wonder why they have to do that??
+ @ini_set('precision', 14); // needed for upgrades and gradebook
+
+
/// The current directory in PHP version 4.3.0 and above isn't necessarily the
/// directory of the script when run from the command line. The require_once()
/// would fail, so we'll have to chdir()