diff options
| author | Clément Pit-Claudel | 2020-01-06 14:10:01 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-01-06 14:10:01 -0500 |
| commit | 1630da989cb0184d50d108ddb3a970f860058fb6 (patch) | |
| tree | d59ebd595b3a92d1538fad5cb4fad8c5dbf9919c /proofs | |
| parent | 95124216fba92f75e0aef97f4c0003eeb8689557 (diff) | |
| parent | 9bbbe5c49951b17d8066ece22f81f8785dbed917 (diff) | |
Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migration.
Reviewed-by: jfehrle
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions