diff options
| author | svn2git <svn2git@FreeBSD.org> | 1994-07-01 08:00:00 +0000 |
|---|---|---|
| committer | svn2git <svn2git@FreeBSD.org> | 1994-07-01 08:00:00 +0000 |
| commit | 5e0e9b99dc3fc0ecd49d929db0d57c784b66f481 (patch) | |
| tree | e779b5a6edddbb949b7990751b12d6f25304ba86 /sys/doc/Makefile | |
| parent | a16f65c7d117419bd266c28a1901ef129a337569 (diff) | |
Diffstat (limited to 'sys/doc/Makefile')
| -rw-r--r-- | sys/doc/Makefile | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/sys/doc/Makefile b/sys/doc/Makefile new file mode 100644 index 000000000000..78e3021c3831 --- /dev/null +++ b/sys/doc/Makefile @@ -0,0 +1,19 @@ +# $Id: Makefile,v 1.1 1994/03/30 20:36:32 wollman Exp $ +# +# Makefile for /sys/i386/doc +# This creates options.info and options.doc from options.texi, if the +# GNU makeinfo program is present, and fails miserably otherwise. +# + +all: options.info options.doc + +options.info: options.texi + makeinfo options.texi + +options.doc: options.texi + makeinfo -o options.doc+ --no-headers options.texi + sed '/^General Index/,$$d' < options.doc+ > options.doc + rm -f options.doc+ + +clean: + rm -f options.info options.doc options.doc+ |