diff options
| author | Pierre Courtieu | 2004-03-10 18:54:34 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2004-03-10 18:54:34 +0000 |
| commit | 41c4820a778903785d2009820a06787d273152e4 (patch) | |
| tree | 50fefbcb5c3bad5b38760cefca04aeee732d3496 /pgshell | |
| parent | 4221aa359e8e32738d502515e1f63be58dc702d5 (diff) | |
fixed coq command-end expression-regexp to deal with the token '..'
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions