diff options
| author | Hugo Herbelin | 2014-12-03 14:48:09 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-03 19:26:16 +0100 |
| commit | 34bb77c953e917f5fbff489c5758abcbadc22224 (patch) | |
| tree | d92ff3dbde50be1227891b7dde96a1ee3951c6ca /dev | |
| parent | dfeaea43d9e692984cf430f4f19ec527625586ea (diff) | |
Slight improving of a unification error message.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions