Hi, I believe I fixed all the issues in the package hol-light.
- I imported a new upstream version, which is distributed now with a BSD 2 clause license - The camlp5 dependencies are right - hol-light is a binary package with a lintian override for arch-dep-package-has-big-usr-share - One test is performed during package build: This tests loads the HOL Light base (in file hol.ml) and the arithmetic-geometric mean example (Library/agm.ml). - The upstream test suite is installed as /usr/share/hol-light/holtest, with instruction on howto run it in README.Debian. - A number of external tools that can be used with HOL Light are in Suggests. Bye, Hendrik -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected] Archive: http://lists.debian.org/[email protected]

