diff options
Diffstat (limited to 'man/GNUmakefile')
| -rw-r--r-- | man/GNUmakefile | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/man/GNUmakefile b/man/GNUmakefile deleted file mode 100644 index 96aa665..0000000 --- a/man/GNUmakefile +++ /dev/null @@ -1,27 +0,0 @@ -# Having a separate GNUmakefile lets me use features of GNU make -# to generate the man pages. -# 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 |