Custom Query (361 matches)
Results (16 - 18 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #485 | fixed | "Time commands" option offsets the cursor when errors are reported | ||
| Description |
When activating the "Time Commands" option, every time an error is displayed, the cursor is off 5 characters to the right. Happens in the latest development build as well as in the last stable. To reproduce, open a buffer and type: Inductive t := T : x -> y -> t.
Try to run it when "Time Commands" is on. The error is reported on the |
|||
| #484 | fixed | [Existing Instances] should be highlighted like [Existing Instance] | ||
| #482 | fixed | [lazymatch] should be highlighted and indented like [match] | ||
| Description |
Currently, it causes the branches to be deindented, and does not match the highlighting of |
|||
Note: See TracQuery
for help on using queries.
