Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Avoid rebuilding cmi_info record when creating .cmti files #781
Instead of rebuilding cmi_info in Cmt_format.save_cmt, the record
The interface is also stronger, since the signature passed to save_cmt
referenced this pull request
Aug 26, 2016
Note that this PR does not change this behavior. One could perhaps use the list of imports from the .cmi instead, but this would make the code less regular (one would still need to call Env.imports when the cmi is not provided).