Merge PR #6909: Deprecate Focus and Unfocus

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2ad4b87f41..0e80215fdc 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,7 @@ Focusing
 - Focusing bracket `{` now supports single-numbered goal selector,
   e.g. `2: {` will focus on the second sub-goal. As usual, unfocus
   with `}` once the sub-goal is fully solved.
+  The `Focus` and `Unfocus` commands are now deprecated.
 
 Vernacular Commands