A while ago I pinched a snippet of PHP from somewhere to use in a session id generator. It all worked fine, but as I was only just starting out in PHP I didn't investigate too deeply how it worked. This construct is now puzzling me: $foo=rand()%(strlen($pool));
The effect is to choose a random number between zero and the character length of string $pool - yet I can't find any documentation on this form of rand() anywhere... the manual for PHP4 specifies rand(min_value, max_value) for this kind of thing.
Does anyone know if this is a correct construct or a hangover from an earlier version of PHP?