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 /Makefile.extr | |
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 'Makefile.extr')
0 files changed, 0 insertions, 0 deletions