Opened 10 years ago

Closed 10 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:



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.


Hendrik Tews

Change History (1)

comment:1 Changed 10 years ago by David Aspinall

Resolution: fixed
Status: newclosed

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.