diff options
| author | Clément Pit-Claudel | 2018-09-24 09:10:47 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-09-24 09:10:47 -0400 |
| commit | fb8365e96ccb5d25d3810af99c36e7b27fec8fad (patch) | |
| tree | c516748b678652f998851e13c2f48477a0ca8787 /dev | |
| parent | c2a1cc7473cf4db27ee47ac011409f7a1839b36d (diff) | |
| parent | a454d1dc509aae06eadf7474eb25e90abdf36ca1 (diff) | |
Merge PR #8541: Update flag, option and table descriptions in coqdomain.py, update README.rst to match.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions