fix(index) Fix phpCas server port type

There is a wrong type in phpCas phpdoc in some versions (1.3.6 from
 debian is affected)

issue #6114