diff options
| author | David Aspinall | 1999-09-13 14:00:51 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-09-13 14:00:51 +0000 |
| commit | ad90401f1d922a03bf7317836c6a40eae81739c2 (patch) | |
| tree | c5de8cfba657059e79bd6feb130403958e6857df /doc/Makefile | |
| parent | 104b96ed7a160b16492b9fadc00f35dcdba49d94 (diff) | |
Fix so that buffer names are shorter (esp for Coq).
A fixed version of Patrick's earlier patch.
Diffstat (limited to 'doc/Makefile')
0 files changed, 0 insertions, 0 deletions