diff --git a/mps/Makefile.in b/mps/Makefile.in index 743a1cfe6cd..627817ea40d 100644 --- a/mps/Makefile.in +++ b/mps/Makefile.in @@ -67,6 +67,11 @@ Makefile: $(srcdir)/Makefile.in config.status clean: @CLEAN_TARGET@ config.status: $(srcdir)/configure + if [ -x config.status ]; then \ + ./config.status --recheck; \ + else \ + $(srcdir)/configure; \ + fi $(srcdir)/configure: $(srcdir)/configure.ac autoreconf -vif $(srcdir)