diff options
| author | Clément Pit-Claudel | 2020-05-08 15:08:43 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-05-08 15:08:43 -0400 |
| commit | 3d01f120976be6805a80b34633b9cd9552b2ffe3 (patch) | |
| tree | 83edc3c1431b97dd004adf4a771f280f02b97e4f /dev/doc | |
| parent | 343591ce6462543f1ffcdc1bfb0377042027ce12 (diff) | |
| parent | 71d0315f2559dca43a5ea733f91199965b8b7879 (diff) | |
Merge PR #12272: Cleanup formatting in .. coqtop:: directives
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions