[gnome-builder] prefs: add option for parallel build workers

[Christian Hergert <chergert src gnome org>]

commit d110043614b8ecdee18fbecdbbb7a7683e604f72
Author: Christian Hergert <chergert redhat com>
Date:   Wed Dec 23 00:53:38 2015 -0800

    prefs: add option for parallel build workers

 libide/preferences/ide-preferences-builtin.c |   10 ++++++++++
 1 files changed, 10 insertions(+), 0 deletions(-)
---
diff --git a/libide/preferences/ide-preferences-builtin.c b/libide/preferences/ide-preferences-builtin.c
index 4d29c29..9aabb17 100644
--- a/libide/preferences/ide-preferences-builtin.c
+++ b/libide/preferences/ide-preferences-builtin.c
@@ -320,6 +320,15 @@ ide_preferences_builtin_register_languages (IdePreferences *preferences)
   ide_preferences_add_radio (preferences, "languages.id", "indentation", 
"org.gnome.builder.editor.language", "auto-indent", "/org/gnome/builder/editor/language/{id}/", NULL, 
_("Automatically indent"), _("Indent source code as you type"), NULL, 30);
 }
 
+static void
+ide_preferences_builtin_register_build (IdePreferences *preferences)
+{
+  ide_preferences_add_page (preferences, "build", _("Build"), 500);
+
+  ide_preferences_add_list_group (preferences, "build", "basic", _("General"), 0);
+  ide_preferences_add_spin_button (preferences, "build", "basic", "org.gnome.builder.build", "parallel", 
"/org/gnome/builder/build/", _("Build Workers"), _("Number of parallel build workers"), NULL, 0);
+}
+
 void
 _ide_preferences_builtin_register (IdePreferences *preferences)
 {
@@ -331,4 +340,5 @@ _ide_preferences_builtin_register (IdePreferences *preferences)
   ide_preferences_builtin_register_keyboard (preferences);
   ide_preferences_builtin_register_vcs (preferences);
   ide_preferences_builtin_register_plugins (preferences);
+  ide_preferences_builtin_register_build (preferences);
 }