From b8ef92b33d767f8d319e34799d4b95e05c73d368 Mon Sep 17 00:00:00 2001 From: CharlesCNorton <135471798+CharlesCNorton@users.noreply.github.com> Date: Sat, 14 Dec 2024 18:11:36 -0500 Subject: [PATCH] Fix typos and grammar: README.md -Corrected "only recompiling files that need to be," to "only recompile files that need to be," for grammatical accuracy. -Fixed "no lot is included" to "no log is included" to resolve a typo. --- rocq-tools/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/rocq-tools/README.md b/rocq-tools/README.md index 9d445d0f..71e11415 100644 --- a/rocq-tools/README.md +++ b/rocq-tools/README.md @@ -6,7 +6,7 @@ and performance data while compiling Coq projects efficiently with dune. As it is not currently possible to teach `dune` about custom data files (or any form of additional file generated by compilation), we embed the generated data into `.glob` files. With this approach, we both get: -1. fast CI using the dune cache to only recompiling files that need to be, +1. fast CI using the dune cache to only recompile files that need to be, 2. additional data for all files, including those that hit the cache. Data Gathering @@ -48,7 +48,7 @@ several pieces of data, which are all embedded into `.glob` files: the performance numbers for the whole file is also included. - A JSON log produced by our custom logger library if it was used (either from a plugin, or from our corresponding Ltac2 library). If the logger library is - not in use, no lot is included. + not in use, no log is included. - A copy of what the wrapped invocation of `coqc` printed on its `stderr`, and (separately) on its `stdout`. This is useful for, e.g., listing the warnings produced by the compilation of a given file, in case the cache hits.