Possible licensing problem of otherslibs/num

[Jérôme Marant <jmarant@free.fr>]

Hi,

I was noticed by someone in IRC #ocaml of otherslibs/num/README where
we can read:

-=-=-=-=-=-

LEGAL NOTICE:

This work uses the BigNum package developed jointly by INRIA and Digital PRL.

The code in the bignum/ subdirectory is copyright INRIA and Digital,
and may be reproduced and distributed freely to non commercial usage
according to the conditions stated in the documentation of this package
(directory bignum/doc).

-=-=-=-=-=-

Yet another licensing issue?

-- 
Jérôme Marant