diff options
| author | Makarius Wenzel | 2000-02-07 10:05:32 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-02-07 10:05:32 +0000 |
| commit | 7f0aca40899e3758402816b7d681d02a8ee7e6e3 (patch) | |
| tree | 2fe15943aaf709ef12b7a424223ff7cb29bbb5ef /html | |
| parent | d33aa4753f3447f70ee725b7576e0dc12678209b (diff) | |
fixed proof-shell-error-regexp;
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions