if (inf == -1)
fprintf (output, "(00 00 00 00 00 00 f0 ff)"); /* negative infinity */
else if (inf == 1)
fprintf (output, "(00 00 00 00 00 00 f0 7f)"); /* positive infinity */
if (inf == -1)
fprintf (output, "(00 00 00 00 00 00 f0 ff)"); /* negative infinity */
else if (inf == 1)
fprintf (output, "(00 00 00 00 00 00 f0 7f)"); /* positive infinity */