diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-11-27 16:58:27 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-27 16:58:27 +0100 |
| commit | 5d4cba919a915eb76251173aabcc2332a44adc70 (patch) | |
| tree | b5d37ee87278989abb57e100f7c22f9c8d7ed3db /common | |
| parent | 12f7b21e6e1bafe895680108e75311c678a22ac1 (diff) | |
| download | compcert-5d4cba919a915eb76251173aabcc2332a44adc70.tar.gz compcert-5d4cba919a915eb76251173aabcc2332a44adc70.zip | |
Remove temporary .o files after linking (#36)
When -c is not given, .o files are now generated in /tmp, but they are still not erased.
This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits.
Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
Diffstat (limited to 'common')
0 files changed, 0 insertions, 0 deletions