aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile.extr
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-03-07 11:51:25 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-03-07 11:51:25 +0100
commit3e01154d693e1c457e1e974f5e9ebaa4601050aa (patch)
tree3f4fde8ba8c3179e5c2b274b115ca8e00cbda37a /Makefile.extr
parentd3959ce85c17d31921c0e3143b58734e090002f0 (diff)
parent70b3b1cb30c9af476d23ceb61d0acd8342d56bfa (diff)
downloadcompcert-3e01154d693e1c457e1e974f5e9ebaa4601050aa.tar.gz
compcert-3e01154d693e1c457e1e974f5e9ebaa4601050aa.zip
Merge branch 'master' of https://github.com/AbsInt/CompCert
Diffstat (limited to 'Makefile.extr')
-rw-r--r--Makefile.extr4
1 files changed, 0 insertions, 4 deletions
diff --git a/Makefile.extr b/Makefile.extr
index eb578fa9..fed2d78f 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -158,10 +158,6 @@ clean:
rm -f $(GENERATED)
for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
-cleansource:
- rm -f $(EXECUTABLES)
- for d in $(ALLDIRS); do rm -f $$d/*.cm[iox] $$d/*.o; done
-
# Generation of .depend.extr
depend: $(GENERATED)