diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-01 15:27:16 +0100 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-12-01 15:27:16 +0100 |
commit | 7b0ce5abd6a31a3790dfcfd3be69064bd5ca5eb3 (patch) | |
tree | c2d0e98a599f1ad3a87a866f2e273f92b82e291d /runtime | |
parent | 0c84a608141523ac6f4c12cb8183eff3bfa42039 (diff) | |
download | compcert-7b0ce5abd6a31a3790dfcfd3be69064bd5ca5eb3.tar.gz compcert-7b0ce5abd6a31a3790dfcfd3be69064bd5ca5eb3.zip |
Allow relative paths for the tools.
The tools now can be specified by 3 ways:
-Relative to the compcert.ini file
-With absolute path to the location
-As a simple filename which lies on the PATH variable.
Bug 17431
Diffstat (limited to 'runtime')
0 files changed, 0 insertions, 0 deletions