diff options
| author | Pierre Courtieu | 2015-11-13 16:38:28 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2015-11-13 16:38:28 +0100 |
| commit | 72f6fbe94fd3a90646c757cf5a76cfae50ac96bc (patch) | |
| tree | 7e92b250af71147bf471b6d09fb19adff41fbf26 /pgshell | |
| parent | 95c86b944368015804f0bfd0002dc098578bda58 (diff) | |
compilation fix (coq-pre-v85).
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions