diff --git a/mps/configure b/mps/configure index f29a67b3fad..06570f5a2bf 100755 --- a/mps/configure +++ b/mps/configure @@ -4019,3 +4019,5 @@ if test -n "$ac_unrecognized_opts" && test "$enable_option_checking" != no; then $as_echo "$as_me: WARNING: unrecognized options: $ac_unrecognized_opts" >&2;} fi + +echo 1>&2 "CONFIGURE/MAKE IS NOT THE BEST WAY TO BUILD THE MPS -- see " diff --git a/mps/configure.ac b/mps/configure.ac index 02d16a9c0a3..19855c7e656 100644 --- a/mps/configure.ac +++ b/mps/configure.ac @@ -96,3 +96,5 @@ AC_SUBST(CFLAGS) AC_CONFIG_FILES(Makefile example/scheme/Makefile) AC_OUTPUT + +echo 1>&2 "CONFIGURE/MAKE IS NOT THE BEST WAY TO BUILD THE MPS -- see "