meson: make doc build optional

Make it possible to disable the documentation build by passing,

  $ meson setup -Dbuild-docs=false

Otherwise, the documentation will be built by default, as usual.

Author: orlitzky

meson.options

@@ -7,3 +7,12 @@ option(
   value: '',
   description: 'Path to SAGE_LOCAL directory (only used for compatibility with the old Sage-the-Distro',
 )
+
+#
+# Boolean options
+#
+option(
+  'build-docs',
+  type: 'boolean',
+  description: 'Build the HTML / PDF documentation'
+)

src/doc/meson.build

@@ -1,3 +1,7 @@
+if not get_option('build-docs')
+  subdir_done()
+endif
+
 sphinx_check = py_module.find_installation(required: false, modules: ['sphinx'])
 if not sphinx_check.found()
   warning(
@@ -6,6 +10,7 @@ if not sphinx_check.found()
   subdir_done()
 endif
 
+
 doc_src = []
 subdir('en/reference/repl')
 # TODO: Migrate this completely to meson