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 /.depend | |
| 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 '.depend')
0 files changed, 0 insertions, 0 deletions