diff options
Diffstat (limited to 'mpi-patches/disable-make')
| -rw-r--r-- | mpi-patches/disable-make | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/mpi-patches/disable-make b/mpi-patches/disable-make new file mode 100644 index 00000000..04e53d3d --- /dev/null +++ b/mpi-patches/disable-make @@ -0,0 +1,18 @@ +Index: mpi-1.8.6/Makefile +=================================================================== +--- mpi-1.8.6.orig/Makefile 2012-04-10 20:41:06.333743757 -0700 ++++ mpi-1.8.6/Makefile 2012-04-10 20:43:28.337576007 -0700 +@@ -14,6 +14,13 @@ + ## 'mpi-config.h', which you should set as appropriate. + ## + ++.PHONY: all ++all: ++ @echo "Do not use this Makefile! TXR pulls in the MPI sources into" ++ @echo "its own build environment. If something isn't working" ++ @echo "it has to be debugged properly." ++ exit 1 ++ + include Makefile.base + + ###---------------------------------------------------------------------- |