diff options
| author | Clément Pit-Claudel | 2020-05-08 22:10:58 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-05-09 17:23:43 -0400 |
| commit | 2f74daa02ac02d63f3f755c36b0749c8f91eb733 (patch) | |
| tree | 13fe712365ddf79f00de5e3107c1ee8a323a3f7f /doc/LICENSE | |
| parent | 3d01f120976be6805a80b34633b9cd9552b2ffe3 (diff) | |
[sphinx] Add links to other versions of the refman
Diffstat (limited to 'doc/LICENSE')
| -rw-r--r-- | doc/LICENSE | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index 9f3a6b3f4c..a327156144 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -6,13 +6,16 @@ copyright (c) 1999-2019, Inria, CNRS and contributors, with the exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font license, version 1.0 -(https://www.ubuntu.com/legal/terms-and-policies/font-licence), and +(https://www.ubuntu.com/legal/terms-and-policies/font-licence), its derivative CoqNotations.ttf distributed under the same -license. The material connected to the Reference Manual may be -distributed only subject to the terms and conditions set forth in the -Open Publication License, v1.0 or later (the latest version is -presently available at http://www.opencontent.org/openpub/). Options -A and B are *not* elected. +license, and the _templates/versions.html file derived from +sphinx_rtd_theme, which is Copyright 2013-2018 Dave Snider, Read the +Docs, Inc. & contributors and distributed under the MIT License +included in that file. The material connected to the Reference Manual +may be distributed only subject to the terms and conditions set forth in +the Open Publication License, v1.0 or later (the latest version is +presently available at http://www.opencontent.org/openpub/). Options A +and B are *not* elected. The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source |