diff options
| author | Enrico Tassi | 2014-10-22 16:18:19 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-22 16:18:19 +0200 |
| commit | 5e3a56c233ad412b96ce473cf775f6b7bd9e72f7 (patch) | |
| tree | c0a78d0e1b5c9bd74b69a530261102da236636d5 /kernel/nativecode.ml | |
| parent | 39d9b466b1d270bf0003bffa12193423aaa31696 (diff) | |
Make rint_location_in_file resilient to Cd (close 3630)
Cd can make the relative path of the opened file wrong,
and hence not available anymore when we reopen it to compute
the line number.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions