diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-11 10:16:11 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-11 10:16:11 +0200 |
| commit | 3e69cc44b2a7430881b4425cb5d543c888d9b4c7 (patch) | |
| tree | a1038c42d2e79cd4a9065310fc661e29edeb6791 /engine/nameops.ml | |
| parent | 09ba1e86504c5df554c3bdd1eae05bddcafc6ef2 (diff) | |
| parent | 577738531f607da8e6347ade1dc3767d98aaf863 (diff) | |
Merge PR #7203: removing ugly error message of #5147
Diffstat (limited to 'engine/nameops.ml')
0 files changed, 0 insertions, 0 deletions