PGAGetMaxMachineDoubleValue(3) on Linux

The text 506e6b04e60e, as Debian 1.1 (Buzz) shipped it.

returns the largest double of the current machine

PGAGetMaxMachineDoubleValue(3) on Linux now