diff options
author | Colin Walters <walters@verbum.org> | 2012-11-13 13:05:55 -0500 |
---|---|---|
committer | Matthias Clasen <mclasen@redhat.com> | 2012-11-19 20:49:37 -0500 |
commit | 2cc0b7023b78e3bd9e111c8b0a719c4d10dde5cf (patch) | |
tree | b2cf79bcc6372852188236b32e1cf34af6eb7ac8 /doc | |
parent | 121067a005a1bb65bdb86534274a8a8658d57f09 (diff) | |
download | gnome-session-2cc0b7023b78e3bd9e111c8b0a719c4d10dde5cf.tar.gz |
build: Add --disable-man option
1) For embedded systems, it makes no sense to include documentation
of this kind on each image. So we might as well not even build
it.
2) For people bootstrapping systems from source code, documentation
is the source of many cyclical build loops. Allowing it to
be disabled helps cut these loops.
3) The Docbook stylesheets and build system have no sane upstream,
and so at the moment aren't included in gnome-ostree.
https://bugzilla.gnome.org/show_bug.cgi?id=688271
Diffstat (limited to 'doc')
-rw-r--r-- | doc/Makefile.am | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/doc/Makefile.am b/doc/Makefile.am index 04f4e978..1129c415 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -1,3 +1,7 @@ -SUBDIRS = dbus man +SUBDIRS = dbus + +if ENABLE_MAN +SUBDIRS += man +endif -include $(top_srcdir)/git.mk |