| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fix Hint (Transparent | Opaque) index.
|
|
Add some more cmd references.
And use deprecated directives.
|
|
|
|
|
|
|
|
In particular, remove trailing dots.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
All the error messages start with a capitalized letter and end with a dot.
|
|
|
|
- Remove all trailing dots.
- There is only one Bullet Behavior option.
- Replaces `@natural` and `@integer` by `@num`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
|
|
(cf. 6131f89f6b91c45e641dd877df8719fa77987453)
|
|
|
|
|
|
We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.
Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.
Closes #6689.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #6963.
|
|
|
|
|
|
|
