Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

License: unclear #496

Closed
SnarkBoojum opened this issue Jul 9, 2022 · 2 comments · Fixed by #510
Closed

License: unclear #496

SnarkBoojum opened this issue Jul 9, 2022 · 2 comments · Fixed by #510

Comments

@SnarkBoojum
Copy link

I packaged coq-equations for Debian, but it got rejected because of licensing issues: the file headers says LGPL 2.1, the opam says LGPL-2.1+.

There are files (theories//Relation.v) out of coq: they are LGPL-2.1.

Could you clarify? Thanks.
@mattam82
Copy link
Owner

It is LGPL-2.1, I don't know why the or-later popped up in the opam package.

@palmskog
Copy link
Contributor

palmskog commented Sep 9, 2022 •
edited

The origin of the LGPL-2.1-or-later is a suggestion by me to try to clarify the ambiguous "LGPL 2.1": coq/opam#999

However, it was just a suggestion, it was approved by @mattam82. So maybe we can clarify once and for all, and I'll update the opam archive: the SPDX identifier of the Equations license is LGPL-2.1-only?

@palmskog palmskog mentioned this issue Sep 9, 2022
Merged
@palmskog palmskog mentioned this issue Sep 19, 2022
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

set license to LGPL-2.1-only in coq-equations.opam palmskog/Coq-Equations
3 participants
@mattam82 @palmskog @SnarkBoojum