diff options
| author | David Aspinall | 2001-08-30 14:18:16 +0000 |
|---|---|---|
| committer | David Aspinall | 2001-08-30 14:18:16 +0000 |
| commit | 1ae6589f077f76de8d279ac5fc5d4301792ba51e (patch) | |
| tree | 8a27d714d9ce5df67e0b69b9caa5534fd8010446 /generic/proof-script.el | |
| parent | a1acb2a34bb28aaaa4270cd5ebda7fcad52cb897 (diff) | |
pg-insert-last-output-as-comment strips special annotations from last output before inserting as comment.
Diffstat (limited to 'generic/proof-script.el')
0 files changed, 0 insertions, 0 deletions