diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-08-23 19:43:14 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-08-23 19:43:14 +0200 |
| commit | c879cd9abb6e5dac1bc303da1b0c11e551d8528e (patch) | |
| tree | a72504985b0a5f5e4ac2971b4f853b4085985826 /debug | |
| parent | c6567a3f0a16050fd04469fdcc7a575f81c0c8f4 (diff) | |
| download | compcert-c879cd9abb6e5dac1bc303da1b0c11e551d8528e.tar.gz compcert-c879cd9abb6e5dac1bc303da1b0c11e551d8528e.zip | |
Added the directory ../share/compcert to the search path for .ini files and replaced the if else for the different possibilities by a List.find.
Diffstat (limited to 'debug')
0 files changed, 0 insertions, 0 deletions