diff options
| author | David Aspinall | 2000-06-06 13:59:52 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-06-06 13:59:52 +0000 |
| commit | 193adb101d6c0eb6c1e7d73835ba25b0807faa09 (patch) | |
| tree | 944dfeb0c4ed5c82659874864d61d57bec1c0403 /generic | |
| parent | e2d9c99d148bdbfd42ef80a09512b735a0209818 (diff) | |
Allowed ; to terminate a command by including it in regexp for cmdstart
Added completion for Isar keywords and X-symbol token names.
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions