diff options
| author | Pierre Courtieu | 2006-07-04 08:41:08 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-07-04 08:41:08 +0000 |
| commit | e110e3388866ebc48f15200eb8adcfd46043aad7 (patch) | |
| tree | 9439edda08c511a7721b2b4421ee1955cec5c0a1 /pgshell/README | |
| parent | 3c2c9defa1632ad3c99e4696222f148487b73a6e (diff) | |
moving coq-goal-command-p to indetation code, as from v8.1, goals are
detected by the goal attribute of spans. syntactical goal recognizing
is still used in indetation code, and for v8.0 compatibility. I shall
remove v8.0 compatibility in some months.
Diffstat (limited to 'pgshell/README')
0 files changed, 0 insertions, 0 deletions