doc: add token error change to RELEASES.md (#2579)

leanprover · Sep 26, 2023 · c7a9829 · c7a9829
1 parent 2ac782c
commit c7a9829
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/RELEASES.md b/RELEASES.md
@@ -14,6 +14,8 @@ v4.2.0 (development in progress)
 v4.1.0
 ---------
 
+* The error positioning on missing tokens has been [improved](https://github.com/leanprover/lean4/pull/2393). In particular, this should make it easier to spot errors in incomplete tactic proofs.
+
 * After elaborating a configuration file, Lake will now cache the configuration to a `lakefile.olean`. Subsequent runs of Lake will import this OLean instead of elaborating the configuration file. This provides a significant performance improvement (benchmarks indicate that using the OLean cuts Lake's startup time in half), but there are some important details to keep in mind:
   + Lake will regenerate this OLean after each modification to the `lakefile.lean` or `lean-toolchain`. You can also force a reconfigure by passing the new `--reconfigure` / `-R` option to `lake`.
   + Lake configuration options (i.e., `-K`) will be fixed at the moment of elaboration. Setting these options when `lake` is using the cached configuration will have no effect. To change options, run `lake` with `-R` / `--reconfigure`.