[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[bug#38965] [PATCH 04/12] gnu: coq: Reword several comments.
From: |
Brett Gilio |
Subject: |
[bug#38965] [PATCH 04/12] gnu: coq: Reword several comments. |
Date: |
Mon, 06 Jan 2020 02:27:00 -0600 |
>From 0a7b050f58b9f9a014e6512e0b12a0ed1e0f813b Mon Sep 17 00:00:00 2001
From: Brett Gilio <address@hidden>
Date: Mon, 6 Jan 2020 01:34:23 -0600
Subject: [PATCH 04/12] gnu: coq: Reword several comments.
To: address@hidden
* gnu/packages/coq.scm (coq): Reword several comments to improve readability.
---
gnu/packages/coq.scm | 10 +++++-----
1 file changed, 5 insertions(+), 5 deletions(-)
diff --git a/gnu/packages/coq.scm b/gnu/packages/coq.scm
index ce65ed82c8..f0869b0d90 100644
--- a/gnu/packages/coq.scm
+++ b/gnu/packages/coq.scm
@@ -95,8 +95,8 @@
(lambda* (#:key outputs #:allow-other-keys)
(let* ((out (assoc-ref outputs "out"))
(bin (string-append out "/bin")))
- ;; These are exact copies of the version without the .opt
suffix.
- ;; Remove them to save 35 MiB in the result
+ ;; These files are exact copies without `.opt` extension.
+ ;; Removing these saves 35 MiB in the resulting package.
(delete-file (string-append bin "/coqtop.opt"))
(delete-file (string-append bin "/coqidetop.opt")))
#t))
@@ -112,9 +112,9 @@
(lambda _
(with-directory-excursion "test-suite"
;; These two tests fail.
- ;; This one fails because the output is not formatted as
expected.
+ ;; Fails because the output is not formatted as expected.
(delete-file-recursively "coq-makefile/timing")
- ;; This one fails because we didn't build coqtop.byte.
+ ;; Fails because we didn't build coqtop.byte.
(delete-file-recursively "coq-makefile/findlib-package")
(invoke "make")))))))
(home-page "https://coq.inria.fr")
@@ -123,7 +123,7 @@
"Coq is a proof assistant for higher-order logic, which allows the
development of computer programs consistent with their formal specification.
It is developed using Objective Caml and Camlp5.")
- ;; The code is distributed under lgpl2.1.
+ ;; The source code is distributed under lgpl2.1.
;; Some of the documentation is distributed under opl1.0+.
(license (list license:lgpl2.1 license:opl1.0+))))
--
2.24.1
- [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 01/12] gnu: Add ocaml-cairo2., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 03/12] gnu: coq: Update to 8.10.2., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 02/12] gnu: Add ocaml-lablgtk3., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 04/12] gnu: coq: Reword several comments.,
Brett Gilio <=
- [bug#38965] [PATCH 05/12] gnu: coq-flocq: Update to 3.2.0., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 08/12] gnu: coq-gappa: Use HTTPS home page URI., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 06/12] gnu: coq-flocq: Use HTTPS home page URI., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 07/12] gnu: coq-gappa: Update to 1.4.2., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 09/12] gnu: coq-coquelicot: Update to 3.0.3., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 10/12] gnu: coq-coquelicot: Truncate home-page., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 12/12] gnu: coq-equations: Update to 1.2.1., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 11/12] gnu: coq-interval: Update to 3.4.1., Brett Gilio, 2020/01/06
- [bug#38965] [PATCH 00/12] gnu: coq: Update to 8.10.2., Julien Lepiller, 2020/01/06