[gedit] build: rename option user-documentation -> user_documentation

[Sébastien Wilmet <swilmet src gnome org>]

commit 9b226789dccadfab4beb77c6ad818931759a6164
Author: Sébastien Wilmet <swilmet gnome org>
Date:   Tue Nov 19 15:26:31 2019 +0100

    build: rename option user-documentation -> user_documentation
    
    The convention is to have underscores for options. For example that's
    what GLib uses (GLib can serve as a reference point).

 meson.build       | 4 ++--
 meson_options.txt | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)
---
diff --git a/meson.build b/meson.build
index 75900be46..82e3c8551 100644
--- a/meson.build
+++ b/meson.build
@@ -175,7 +175,7 @@ endif
 
 subdir('docs')
 
-if get_option('user-documentation')
+if get_option('user_documentation')
   subdir('help')
 endif
 
@@ -185,7 +185,7 @@ summary = [
   'gedit @0@ (@1@)'.format(version, api_version),
   '',
   '       API docs: @0@'.format(build_gtk_doc),
-  '      User docs: @0@'.format(get_option('user-documentation')),
+  '      User docs: @0@'.format(get_option('user_documentation')),
   '  Introspection: @0@'.format(generate_gir),
   '        Plugins: @0@'.format(build_plugins),
   '       Vala API: @0@'.format(generate_vapi),
diff --git a/meson_options.txt b/meson_options.txt
index 22aa0899c..bc8272d92 100644
--- a/meson_options.txt
+++ b/meson_options.txt
@@ -15,6 +15,6 @@ option('documentation',
        description: 'Build API reference for plugins (requires gtk-doc)')
 
 # This option exists for the developers, to speed up the install.
-option('user-documentation',
+option('user_documentation',
        type: 'boolean', value: true,
        description: 'Build user documentation')