diff options
author | Colin Watson <cjwatson@debian.org> | 2019-03-03 23:31:01 +0000 |
---|---|---|
committer | Colin Watson <cjwatson@debian.org> | 2019-03-03 23:31:01 +0000 |
commit | 1e5d05d668a451a8628fb8222f78897598c71e9a (patch) | |
tree | 3047c43ba2974e67f9a4cad4f36154b903f0a116 /manual | |
parent | 127eaa9f496b6cf33b75a30658ae2436138c9df0 (diff) |
Add configure option to disable building manual
* m4/man-arg-manual.m4: New file.
* configure.ac: Add MAN_ARG_MANUAL.
* manual/Makefile.am: Perform most rules only if BUILD_MANUAL is true.
* manual/intro.me (Arguments to configure): Add --disable-manual.
* README (Non-generic arguments to configure): Update.
* NEWS: Document this.
Diffstat (limited to 'manual')
-rw-r--r-- | manual/Makefile.am | 3 | ||||
-rw-r--r-- | manual/intro.me | 3 |
2 files changed, 6 insertions, 0 deletions
diff --git a/manual/Makefile.am b/manual/Makefile.am index 783ab2aa..6cf339ea 100644 --- a/manual/Makefile.am +++ b/manual/Makefile.am @@ -39,6 +39,8 @@ dist_noinst_DATA = \ $(ME_FILES) \ options-only.me \ print-options + +if BUILD_MANUAL noinst_DATA = \ $(MANUAL).cat \ $(MANUAL).ps @@ -103,3 +105,4 @@ install-data-hook: uninstall-hook: rm -rf "$(DESTDIR)$(docdir)" +endif diff --git a/manual/intro.me b/manual/intro.me index e83de89c..a2b45722 100644 --- a/manual/intro.me +++ b/manual/intro.me @@ -315,6 +315,9 @@ Normally, will automatically try to create cat files corresponding to manual files when a manual page is read. This flag suppresses this behaviour. +.ip \-\-disable\-manual +Don't build or install the \*M manual. +This may be useful when cross-compiling, or to reduce the installation size. .if r MAN-OPTIONS-ONLY \{ .lp MAN\-OPTIONS\-END |