[Bug 719150] Review Request: flocq - Formalization of floating point numbers for Coq

bugzilla at redhat.com bugzilla at redhat.com
Wed Oct 26 19:39:44 UTC 2011

Please do not reply directly to this email. All additional
comments should be made in the comments box of this bug.


Thomas Spura <tomspur at fedoraproject.org> changed:

           What    |Removed                     |Added
                 CC|                            |tomspur at fedoraproject.org

--- Comment #1 from Thomas Spura <tomspur at fedoraproject.org> 2011-10-26 15:39:43 EDT ---

- group ok
- License ok
- rpmling ignorable/expected warnings
$ rpmlint /home/tom/rpmbuild/RPMS/x86_64/flocq-1.4.0-1.fc15.x86_64.rpm
flocq.x86_64: W: spelling-error %description -l en_US multi -> mulch, mufti
flocq.x86_64: W: spelling-error %description -l en_US radix -> radii, radio,
rad ix
flocq.x86_64: E: no-binary
flocq.x86_64: W: only-non-binary-in-usr-lib
flocq.src: W: spelling-error %description -l en_US multi -> mulch, mufti
flocq.src: W: spelling-error %description -l en_US radix -> radii, radio, rad
flocq.src:30: W: configure-without-libdir-spec
2 packages and 0 specfiles checked; 1 errors, 6 warnings.

- arch ok (needs to be in /usr/lib64 although noarch)
- %files ok
  %{_libdir}/coq/user-contrib/ is owned by coq (a R)

- Please use INSTALL="install -p" for preserving timestamps

Just a few questions, before I'll approve this:
* Don't the source belongs to a devel package like other packages?
  (Don't know how that usually works in ocalm.)
  Or are the sources needed at runtime?

* When the source are needed at runtime, this looks like a bug in the Makefile,
so it should be installed automaticalls isn't it?

Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email
------- You are receiving this mail because: -------
You are on the CC list for the bug.

More information about the package-review mailing list