diff options
| author | Pierre Courtieu | 2006-07-04 17:10:27 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-07-04 17:10:27 +0000 |
| commit | a88b79a4e42bbb2e12e290c46496e3dde162de95 (patch) | |
| tree | 75db69041b6a216ef9168c038c6b46b0ef9e8f10 /pgshell/example.pgsh | |
| parent | dafc82fac00976f0caaaad43d66778759b93827d (diff) | |
fix the bug for coq indetation of two consecutive comments. Code is
ugly, should take the code given by Stefan Monnier and adapt it (it
does not indent everything as is).
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions