diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 09:44:06 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 09:44:06 +0200 |
| commit | 5bac7458e037879142eb468fc4695b996189a20b (patch) | |
| tree | b9865709399d6f5c63d47334eb3b93a4860f89a6 /plugins/setoid_ring | |
| parent | f7be3ebfee41f178b06e7a606ea783a08bfbb0d1 (diff) | |
| parent | d2b1443e6540348e2efa822fe55bb1185c63d8ce (diff) | |
Merge PR #962: Move dev/doc/changes to Markdown.
Diffstat (limited to 'plugins/setoid_ring')
0 files changed, 0 insertions, 0 deletions