diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-03 11:01:16 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-03 11:01:16 +0100 |
commit | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (patch) | |
tree | 2c75844e980840d2d4f25b8a27de936ae3c370f8 /pretyping | |
parent | 96a8d73edaa4eba500c440e5d6869fae1af91a12 (diff) | |
parent | 0f66537db5df9a7f5ba9a056fd21ff34e83cc8dc (diff) |
Merge PR #6060: Improve error message and fix #6055 (spelling mistake).
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions