You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 5640 Reporter: esther Assigned to:@alainfrisch Status: closed (set by @xavierleroy on 2015-12-11T18:04:54Z) Resolution: fixed Priority: normal Severity: minor Category: typing
Original bug ID: 5640
Reporter: esther
Assigned to: @alainfrisch
Status: closed (set by @xavierleroy on 2015-12-11T18:04:54Z)
Resolution: fixed
Priority: normal
Severity: minor
Category: typing
Bug description
Dual bug as #5639.
The read_cmt function should use open_in_bin instead of open_in.
File typing/cmt_format.ml, line 72
The text was updated successfully, but these errors were encountered: