diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 18:56:17 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 18:56:17 +0100 |
| commit | 1b33b57f56f4d53d20318fe9be97dec274086f5b (patch) | |
| tree | 5ce9d34268d22c3f44303438756e0be83ea3ca99 /dev | |
| parent | a876df3f1e9a495ee04c78321adf83a31ede7f3c (diff) | |
| parent | b5fc7e9e8efc18935d562bd0690c9667fdc8066f (diff) | |
Merge PR #10587: [coqdoc] Nest <a> into <h2> instead of the other way around
Reviewed-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions