diff options
| author | Vincent Laporte | 2019-06-25 07:59:22 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-06-25 07:59:22 +0000 |
| commit | 8fa180ecbd34973f866372bee7bd9020626afedb (patch) | |
| tree | 324bde5c49ad25773d51f7a984f8a1022f314b38 /kernel | |
| parent | 4fe8612fbfd1581b23bb4c813c900ab687797814 (diff) | |
| parent | b883efe3bbb16b5f10f3ecd65b2399233dc00e08 (diff) | |
Merge PR #10408: Fix coqdoc title: should be on a single line.
Reviewed-by: vbgl
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions