diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-24 12:25:30 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-24 12:25:30 +0200 |
| commit | 01354123b9df5d3cbb9d43298eea94ddda30acdf (patch) | |
| tree | 542fa757e835a7331ae229c80cc2e9cafc47ead5 /driver/Linker.ml | |
| parent | 9b31f673da13a4f4d04d937ac2b9e934c9b8291d (diff) | |
| download | compcert-kvx-01354123b9df5d3cbb9d43298eea94ddda30acdf.tar.gz compcert-kvx-01354123b9df5d3cbb9d43298eea94ddda30acdf.zip | |
Deactivate options target dependend.
Options only available for gnu systems or arm target arch are no
longer displayed in the help and cannot be selected any longer.
Bug 19197
Diffstat (limited to 'driver/Linker.ml')
0 files changed, 0 insertions, 0 deletions