[gimp] app: make sure the active tool options get saved in devicerc

[Michael Natterer <mitch src gnome org>]

commit 188fd773a57e99c76e726dbc9345a2acac5ab8d5
Author: Michael Natterer <mitch gimp org>
Date:   Fri Jun 29 02:59:19 2018 +0200

    app: make sure the active tool options get saved in devicerc
    
    gimp_devices_save(): call gimp_device_info_save_tool() on the current
    device.

 app/widgets/gimpdevices.c | 9 +++++++++
 1 file changed, 9 insertions(+)
---
diff --git a/app/widgets/gimpdevices.c b/app/widgets/gimpdevices.c
index 9f52e652dc..efd1131646 100644
--- a/app/widgets/gimpdevices.c
+++ b/app/widgets/gimpdevices.c
@@ -174,6 +174,15 @@ gimp_devices_save (Gimp     *gimp,
   if (gimp->be_verbose)
     g_print ("Writing '%s'\n", gimp_file_get_utf8_name (file));
 
+  if (! GIMP_GUI_CONFIG (gimp->config)->devices_share_tool)
+    {
+      GimpDeviceInfo *current_device;
+
+      current_device = gimp_device_manager_get_current_device (manager);
+
+      gimp_device_info_save_tool (current_device);
+    }
+
   if (! gimp_config_serialize_to_gfile (GIMP_CONFIG (manager),
                                         file,
                                         "GIMP devicerc",