On Thu, Jul 03, 2003 at 02:02:26PM +0800, ZHAO Wei wrote: > I intend to package Moscow ML and later HOL theorem prover for Debian. > This is not a fromal ITP because I'm not eager to prevent others from > doing the same. :) I won't compete with you too. I remember vaguely that there used to be a licence problem with Moscow ML. What is its exact licence now? -Ralf. --