]> matita.cs.unibo.it Git - helm.git/commitdiff
generate gui to temp file in order to catch lablgladecc2 failures
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 17 Dec 2003 14:49:52 +0000 (14:49 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 17 Dec 2003 14:49:52 +0000 (14:49 +0000)
helm/hbugs/client/Makefile

index dc5b3d91f8e55a5179f3c71ce999ece0822ed79d..186931e98211309178083c2fe98fc4cc52dd29c7 100644 (file)
@@ -16,7 +16,8 @@ byte: $(NAME)
 opt: $(NAME).opt
 
 hbugs_client_gui.ml: hbugs_gui.glade
-       lablgladecc2 $< > $@
+       lablgladecc2 $< > $@.tmp
+       mv $@.tmp $@
 hbugs_client_gui.cmo: hbugs_client_gui.ml
        $(OCAMLC) -c $<
 hbugs_client_gui.cmx: hbugs_client_gui.ml