diff options
author | 2009-02-28 12:21:17 +0100 | |
---|---|---|
committer | 2009-02-28 12:25:30 +0100 | |
commit | 77b1735a2a2ecee8988f1d8982fae2d1005f774f (patch) | |
tree | 55f12f9d1ba58674d52c33e26606b4a24f0b726d /pretyping/typing.ml | |
parent | 7fb05c184aa14eb7bed926f30ef81ea5b5ace1dd (diff) |
dh_link expects full targets in *.links file!
Diffstat (limited to 'pretyping/typing.ml')
0 files changed, 0 insertions, 0 deletions