diff options
| author |  Xavier Leroy <xavier.leroy@inria.fr> | 2016-08-14 18:03:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-08-14 18:03:22 +0200 |
| commit | 6d1e0f80d215678559ada3d5b32c22c0d015454e (patch) | |
| tree | 3f2dc794a10f0025f2d19ff993485b297da6cc3b /printing/miscprint.ml | |
| parent | c90c53129436014b0020c52641277d616144282a (diff) | |
Fix regression in Coqide's "forward one command" command
In Coqide 8.5pl2, "forward one command" (down arrow) always repositions the insertion point at the end of the phrase being executed, just after the final ".".
In Coqide 8.4, the insertion point is not moved if it is after the end of the executed phrase. The insertion point is moved only if it falls behind the phrase being executed.
I find the 8.5 behavior to be a regression over the lot more useful 8.4 behavior. This commit restores the 8.4 behavior of "forward one command".
Diffstat (limited to 'printing/miscprint.ml')
0 files changed, 0 insertions, 0 deletions