diff options
| author | Hendrik Tews | 2011-06-08 08:10:31 +0000 |
|---|---|---|
| committer | Hendrik Tews | 2011-06-08 08:10:31 +0000 |
| commit | 710e27c7d9031df0a14727487c83fb6ec974e883 (patch) | |
| tree | c912c6c7826a1b4e61c8c4a4ed1b05d0058a85b4 /pgshell | |
| parent | d5b6bc3e78b4c89f41bd39469f7c6d936e391b97 (diff) | |
- fix for #408: Only use the buffer name in
coq-compile-response-buffer
- fix typo elsewhere
Diffstat (limited to 'pgshell')
0 files changed, 0 insertions, 0 deletions