diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-12 19:04:46 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-12 19:04:46 +0200 |
commit | 57c1eb50c370c894fda1a62ca27d7210982ac3fd (patch) | |
tree | d72479e3469d4968ae916786fba8c4b43f3b0ed0 /ide/serialize.ml | |
parent | e49219e4146a695b46bf1dd8b9580e5fd4cef4ea (diff) | |
parent | 8bb827fd5b979abe17525a6f0256cadb64dd0a23 (diff) |
Merge PR #7202: Correction of ugly message described in #4667
Diffstat (limited to 'ide/serialize.ml')
0 files changed, 0 insertions, 0 deletions