diff options
author | Michael Schmidt <github@mschmidt.me> | 2016-05-10 19:13:18 +0200 |
---|---|---|
committer | Michael Schmidt <github@mschmidt.me> | 2016-05-10 19:13:18 +0200 |
commit | 812ae094557c60847de73c1e9ee198de9c17669d (patch) | |
tree | dfcda11db3d2406623be12d53786b87fa5504617 /debug/Debug.ml | |
parent | 470f207e9229b73dcaea889c531b016a34df3cc5 (diff) | |
download | compcert-812ae094557c60847de73c1e9ee198de9c17669d.tar.gz compcert-812ae094557c60847de73c1e9ee198de9c17669d.zip |
fix typo 'clinker_option' in configure for OSX
Diffstat (limited to 'debug/Debug.ml')
0 files changed, 0 insertions, 0 deletions