diff options
| author | Makarius Wenzel | 1999-10-26 17:30:19 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-10-26 17:30:19 +0000 |
| commit | 99caa19c91e102a97bd97e33fb3e81439671d1db (patch) | |
| tree | 08886f3c79ad9ab9f6b353ccbfcce724646fbc6b /html | |
| parent | e08dcc1bdc8f028a152fb14fbcce91c5632068bb (diff) | |
tuned proof-shell-error-regexp;
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions