|
Make proof-shell-handle-output robust against START-REGEXP match
fail (can happen if shell buffer is garbled/user-edited).
Make proof-shell-insert robust against null STRING (should not
happen; development artefact while getting rid of proof-no-command).
Update date.
|