diff options
Diffstat (limited to 'GNUmakefile')
| -rw-r--r-- | GNUmakefile | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/GNUmakefile b/GNUmakefile new file mode 100644 index 0000000..0c5a071 --- /dev/null +++ b/GNUmakefile @@ -0,0 +1,32 @@ +# 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 + +# Tell version 3.79 and up of GNU make to not build goals in this +# directory in parallel. This is necessary in case someone tries to +# build multiple targets on one command line. +.NOTPARALLEL: |