diff options
| author | Andreas Rumpf <rumpf_a@web.de> | 2019-10-17 20:02:59 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-17 20:02:59 +0200 |
| commit | 81125e2029fdd0d3a9c2931b066bfb72406a21ae (patch) | |
| tree | 753902580f1344727891801d73ec7af51d706084 /doc | |
| parent | 4d1f69c7d253ad9dbe9681062eb650acc9ff5d22 (diff) | |
| download | Nim-81125e2029fdd0d3a9c2931b066bfb72406a21ae.tar.gz | |
[backport] add back a check that got accidentically removed; fixes #12379 (#12444)
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions