diff options
| author | Maxime Dénès | 2017-05-20 01:34:36 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-20 01:34:36 +0200 |
| commit | b7cf93cec115b61889e31c0abefdbd29d9b51ebe (patch) | |
| tree | 8cc84e9c2ae8de301e10d8ea3f2d12303dfb126b /dev | |
| parent | 7dc84057e3596b1c3f6ec869daebcfa8747f5c12 (diff) | |
| parent | 741f3fab052b91eaec57f32b639ca722c3d8dc34 (diff) | |
Merge PR#474: A fix for #5390 (a useful error on used introduction names was masked).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions