diff options
| author | Makarius Wenzel | 2001-12-05 15:36:23 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2001-12-05 15:36:23 +0000 |
| commit | 5721c119ad270b128f8770afbef8a691befd4ed0 (patch) | |
| tree | 73a069664af274cf5c8d91c3c142a0b9c57b116d /html | |
| parent | 990f07fb23220c8294c1090e6d44bd0c5a7dda18 (diff) | |
proof-release-lock: do not touch proof-shell-spill-output-buffer;
proof-shell-spill-output-begin: reuse existing buffer;
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions