diff options
| author | Théo Zimmermann | 2019-06-20 11:43:01 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-06-20 11:43:01 +0200 |
| commit | b883efe3bbb16b5f10f3ecd65b2399233dc00e08 (patch) | |
| tree | 9b8d18dad8ba4b99eb55f94f0d181cea07b8d436 /library | |
| parent | d501690a7d767d4a542867c5b6a65a722fa8c4c1 (diff) | |
Fix coqdoc title: should be on a single line.
Otherwise coqdoc doesn't understand it is still the title.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions