diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2022-11-14 10:24:10 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-11-14 10:24:10 +0100 |
| commit | 5b80eaa2d5141eb4f157d3296b8d92e022386777 (patch) | |
| tree | d376bb1a0471d932f852604b121404bcd2bea082 /cfrontend/Cop.v | |
| parent | d3edf6c07e8a402417323cbeb6d1ef93231c5262 (diff) | |
| download | compcert-5b80eaa2d5141eb4f157d3296b8d92e022386777.tar.gz compcert-5b80eaa2d5141eb4f157d3296b8d92e022386777.zip | |
configure: add option -sharedir to specify where to put compcert.ini (#460)
Make sure that it's one of the three locations where the ccomp executable
looks for compcert.ini.
Closes: #450
Diffstat (limited to 'cfrontend/Cop.v')
0 files changed, 0 insertions, 0 deletions