From 123451d73f19ce13a60437fa225388dea74020c4 Mon Sep 17 00:00:00 2001 From: Segher Boessenkool Date: Mon, 4 Apr 2016 18:37:58 +0200 Subject: [PATCH] gnattools: Clean config.cache (PR70173) The config.cache file should be deleted by "make distclean", just like config.log and config.status . The directory itself is still not deleted (just like the gotools and libcc1 directories). gnattools/ PR bootstrap/70173 * Makefile.in (distclean): Also delete config.cache . From-SVN: r234721 --- gnattools/ChangeLog | 5 +++++ gnattools/Makefile.in | 2 +- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/gnattools/ChangeLog b/gnattools/ChangeLog index bdcd968f308..18aa7021d66 100644 --- a/gnattools/ChangeLog +++ b/gnattools/ChangeLog @@ -1,3 +1,8 @@ +2016-04-04 Segher Boessenkool + + PR bootstrap/70173 + * Makefile.in (distclean): Also delete config.cache . + 2015-12-06 Eric Botcazou PR ada/50048 diff --git a/gnattools/Makefile.in b/gnattools/Makefile.in index 0c889eeec7b..f949ca9b34b 100644 --- a/gnattools/Makefile.in +++ b/gnattools/Makefile.in @@ -309,7 +309,7 @@ mostlyclean: clean: distclean: - $(RM) Makefile config.status config.log + $(RM) Makefile config.status config.log config.cache maintainer-clean: