diff options
| author | Makarius Wenzel | 2000-05-22 09:55:00 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-05-22 09:55:00 +0000 |
| commit | 32c30fd4619963b0c2dd142bcfef7ce89f2db465 (patch) | |
| tree | 644d380ddeac191ec02deb12ffd3ff901e4928f9 /html | |
| parent | 7322f0dde94b563e5600f01789a91fed097433f1 (diff) | |
replaced proof-ids-to-regexp by isar-ids-to-regexp, which admits
keywords to consist of a single non-word char as well (e.g. { });
Diffstat (limited to 'html')
0 files changed, 0 insertions, 0 deletions