From af04dc077741961d77756425ec69fa9d95769723 Mon Sep 17 00:00:00 2001
From: Helmut Eller <eller.helmut@gmail.com>
Date: Fri, 26 Sep 2025 17:50:43 +0200
Subject: [PATCH] * mps/Makefile.in (config.status): Use config.status
 --recheck

---
 mps/Makefile.in | 5 +++++
 1 file changed, 5 insertions(+)

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)