Opened 9 years ago

Closed 9 years ago

#407 closed defect (fixed)

proof-undo-and-delete-last-successful-command does not meet spec

Reported by: Erik Martin-Dorel Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc: Erik Martin-Dorel



I have just noticed the ProofGeneral function proof-undo-and-delete-last-successful-command does not really meet the specification that is described in its documentation, namely:

... the deleted command is put into the Emacs kill ring, so
you can use the usual `yank' and similar commands to retrieve the
deleted text.

I have performed a few tests and it seems sufficient to replace

(proof-undo-last-successful-command-1 'delete-region)


(proof-undo-last-successful-command-1 'kill-region)

in generic/pg-user.el to provide the missing feature.

Kind regards,

Erik Martin-Dorel

Change History (1)

comment:1 Changed 9 years ago by David Aspinall

Resolution: fixed
Status: newclosed

Fixed, many thanks for the report.

Note: See TracTickets for help on using tickets.