diff options
| author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-09-21 15:24:17 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-09-21 15:24:17 +0200 |
| commit | 8fde5790b4f41cec33e994a0f7faa5326e503b7e (patch) | |
| tree | 0b206cde0ab9eff992cf5761d436f69b3c32fba4 /lib/licenses.nix | |
| parent | 3370615a7f1ad927ace45e268b694a184d2ffd43 (diff) | |
compcert: fix license
The license of CompCert is not a generic "INRIA" license. It is "INRIA Non-Commercial Agreement for the CompCert verified compiler". As unfortunate as it may seem, this is a non-free license (clearly mentioned as such in its preamble). See also #20256.
Diffstat (limited to 'lib/licenses.nix')
| -rw-r--r-- | lib/licenses.nix | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/lib/licenses.nix b/lib/licenses.nix index edf35ec035b2c..a790b576032d8 100644 --- a/lib/licenses.nix +++ b/lib/licenses.nix @@ -292,9 +292,10 @@ lib.mapAttrs (n: v: v // { shortName = n; }) rec { fullName = "Independent JPEG Group License"; }; - inria = { - fullName = "INRIA Non-Commercial License Agreement"; + inria-compcert = { + fullName = "INRIA Non-Commercial License Agreement for the CompCert verified compiler"; url = "http://compcert.inria.fr/doc/LICENSE"; + free = false; }; ipa = spdx { |