aboutsummaryrefslogtreecommitdiff
path: root/pgshell/README
diff options
context:
space:
mode:
authorDavid Aspinall2008-01-30 13:44:12 +0000
committerDavid Aspinall2008-01-30 13:44:12 +0000
commit06b34fa6ba4bd78dc67c336b770478369fde45d0 (patch)
tree8fd820c2d7a7d5d9d86d4e99013e284e2648dc77 /pgshell/README
parentc39d6a5ae0f6bc75723a6b36aff96a12123dbb4e (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/README')
0 files changed, 0 insertions, 0 deletions