diff options
| author | David Aspinall | 2008-01-30 13:44:12 +0000 |
|---|---|---|
| committer | David Aspinall | 2008-01-30 13:44:12 +0000 |
| commit | 06b34fa6ba4bd78dc67c336b770478369fde45d0 (patch) | |
| tree | 8fd820c2d7a7d5d9d86d4e99013e284e2648dc77 /pgshell/example.pgsh | |
| parent | c39d6a5ae0f6bc75723a6b36aff96a12123dbb4e (diff) | |
Comment cleanups. buffer-substring -> buffer-substring-no-properties.
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.
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions