diff options
Diffstat (limited to 'GNUmakefile')
| -rw-r--r-- | GNUmakefile | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/GNUmakefile b/GNUmakefile new file mode 100644 index 0000000..0f4e21c --- /dev/null +++ b/GNUmakefile @@ -0,0 +1,27 @@ +# Having a separate GNUmakefile lets me `include' the dynamically +# generated rules created via Makefile.maint as well as Makefile.maint itself. +# This makefile is used only if you run GNU Make. +# It is necessary if you want to build targets usually of interest +# only to the maintainer. + +# Systems where /bin/sh is not the default shell need this. The $(shell) +# command below won't work with e.g. stock DOS/Windows shells. +SHELL = /bin/sh + +have-Makefile := $(shell test -f Makefile && echo yes) + +# If the user runs GNU make but has not yet run ./configure, +# give them a diagnostic. +ifeq ($(have-Makefile),yes) + +include Makefile +include $(srcdir)/Makefile.maint + +else + +all: + @echo There seems to be no Makefile in this directory. + @echo "You must run ./configure before running \`make'." + @exit 1 + +endif |