Comment 5 for bug 1273225

I have reworked the whole php5{en,dis}mod thing and I don't really remember how I reimplemented it :), but the source code helps:

get_priority() {
    local sapi=$1
    local modname=$2

    local source_ini="/etc/php5/mods-available/${modname}.ini"

    module_ret=0
    module_exists $modname || module_ret=$?

    if [ "$module_ret" -eq 0 ]; then
        priority=$(sed -ne "s/^; priority=\([0-9]\+\)$/\\1/p" $source_ini)
        [ -z "$priority" ] && priority=20
        echo $priority
 return 0
    fi

    return $module_ret
}

So yes, the priority is not set from within the .ini.

As for the documentation - patches are always welcome.