Opened 13 years ago

Closed 13 years ago

#396 closed defect (fixed)

error in proof-shell-insert-hook docstring

Reported by: coquser Owned by: David Aspinall
Priority: trivial Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description

Hi,

this docstring mentions the callbacks init-cmd and interactive-input. These seem not to exist any more. It does not mention proof-shell-set-silent and proof-shell-clear-silent.

Bye,

Hendrik Tews

Change History (1)

comment:1 Changed 13 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Thanks, fixed the doc string. Actually, 'init-cmd is still there (but only used in obsolete Lego and not declared as a callback since the init command isn't added to the queue).

Note: See TracTickets for help on using tickets.