diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-04 12:10:31 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-03-05 14:14:25 +0100 |
| commit | ba0a37d773c5d42f96b3b88714767ba2e7fb7a3b (patch) | |
| tree | 5d849636ca0b37d9169c5d4e32610b369439470b /CHANGES | |
| parent | 39ec5b14518c35450aa0d9be2ab1012f5bd2f8e3 (diff) | |
Deprecate Focus and Unfocus.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -60,6 +60,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 |