diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-11-30 17:06:04 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-11-30 17:06:04 +0100 |
| commit | 0c84a608141523ac6f4c12cb8183eff3bfa42039 (patch) | |
| tree | 1d920c818d423ca7b425eaa4998f56fe5d0bc70c /driver/Configuration.mli | |
| parent | 730966facd095f87620aa8d0798ccac7e36aa589 (diff) | |
| download | compcert-0c84a608141523ac6f4c12cb8183eff3bfa42039.tar.gz compcert-0c84a608141523ac6f4c12cb8183eff3bfa42039.zip | |
Allow relative library path.
The path to the libcompert folder can be specified relative to the
location of the compcert.ini file.
Bug 17431
Diffstat (limited to 'driver/Configuration.mli')
0 files changed, 0 insertions, 0 deletions