public static function increment_shortname($shortname) {
        global $DB;
        do {
            $matches = array();
            if (!preg_match('/(.*?)([0-9]+)$/', $shortname, $matches)) {
                $newshortname = $shortname . '_2';
            } else {
                $newshortname = $matches[1] . ($matches[2]+1);
            }
            $shortname = $newshortname;
        } while ($DB->record_exists('course', array('shortname' => $shortname)));
        return $shortname;
    }