[paparazzi-commits] [5876] saveSettings depends on gtk_save_settings

[Allen Ibara]

Revision: 5876
          http://svn.sv.gnu.org/viewvc/?view=rev&root=paparazzi&revision=5876
Author:   aibara
Date:     2010-09-15 03:52:16 +0000 (Wed, 15 Sep 2010)
Log Message:
-----------
saveSettings depends on gtk_save_settings

Modified Paths:
--------------
    paparazzi3/trunk/sw/ground_segment/cockpit/Makefile

Modified: paparazzi3/trunk/sw/ground_segment/cockpit/Makefile
===================================================================
--- paparazzi3/trunk/sw/ground_segment/cockpit/Makefile 2010-09-15 03:51:49 UTC 
(rev 5875)
+++ paparazzi3/trunk/sw/ground_segment/cockpit/Makefile 2010-09-15 03:52:16 UTC 
(rev 5876)
@@ -62,6 +62,9 @@
        @echo OOC $<
        $(Q)$(OCAMLOPT) $(OCAMLCFLAGS) $(INCLUDES) -c $<
 
+saveSettings.cmo : gtk_save_settings.cmo
+saveSettings.cmx: gtk_save_settings.cmx
+
 gtk_strip.ml : gcs.glade
        lablgladecc2 -root eventbox_strip -hide-default $< | grep -B 1000000 "  
end" > $@