diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-08-28 15:40:15 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-08-28 15:40:15 +0200 |
| commit | fa475d37fde87683a38f765588aadac22acf6b93 (patch) | |
| tree | d04597f8c1384536c63683a0dbce6352b6c353eb /LICENSE | |
| parent | 9083177bf96f4f0beef8e5641628d427b5f74344 (diff) | |
| download | compcert-fa475d37fde87683a38f765588aadac22acf6b93.tar.gz compcert-fa475d37fde87683a38f765588aadac22acf6b93.zip | |
Remove leftover Makefile.config before configuration
So that if an error occurs during configuration, there is no
Makefile.config file and "make" will fail.
Closes: #244
Diffstat (limited to 'LICENSE')
0 files changed, 0 insertions, 0 deletions