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

[bugzilla at redhat.com]

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


https://bugzilla.redhat.com/show_bug.cgi?id=719150

--- Comment #4 from Jerry James <loganjerry at gmail.com> 2011-10-26 17:39:49 EDT ---
(In reply to comment #3)
> Sounds like you should do a packaging draft and send it to fpc.
> Maybe further extending this one for Coq add-ons:
> https://fedoraproject.org/wiki/Packaging/OCaml

That's a good idea.  It would be good to have other people's eyes on the way
I'm packaging this stuff, to see if they spot any problems.

> New no-go:
> %files
> %dir %{flocqdir}
> 
> That's already owned by coq, so this shoudn't own it.

No, coq owns the parent directory, %{_libdir}/coq/user-contrib.  The flocqdir
macro expands to %{_libdir}/coq/user-contrib/Flocq.

> APPROVED

Thank you very much for the review.  I appreciate 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.