diff options
| author | Pierre-Marie Pédrot | 2019-10-11 15:52:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-11 15:52:06 +0200 |
| commit | f41cb3d7206155c8ad7321ff76e58bf5bd079c89 (patch) | |
| tree | a5af16ca456ac5a3c966d5b8fd4e724f4d5b1c8e /tools | |
| parent | 649ee5836fe73d5c4e067906092b856c4b6337c2 (diff) | |
| parent | 22e31fd906097a27abc8f659cec9b2102af52bb4 (diff) | |
Merge PR #10740: More precise error messages for `Add Ring`
Reviewed-by: ppedrot
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions