From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 4 Sep 2003 16:45:44 +0000 (+0000)
Subject: avoid deletion of useful .cmi with .PRECIOUS
X-Git-Tag: v0_0_1~44
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=811c9c106279d504c214b54a267b62653d685945

avoid deletion of useful .cmi with .PRECIOUS
---

diff --git a/helm/hbugs/tutors/Makefile b/helm/hbugs/tutors/Makefile
index a585b0c38..fed96f966 100644
--- a/helm/hbugs/tutors/Makefile
+++ b/helm/hbugs/tutors/Makefile
@@ -6,6 +6,7 @@ COMMONOPTS = -package "$(REQUIRES)" -predicates "$(PREDICATES)"
 OCAMLFIND = ocamlfind
 OCAMLC = $(OCAMLFIND) ocamlc $(COMMONOPTS)
 OCAMLOPT = $(OCAMLFIND) opt $(COMMONOPTS)
+OCAMLDEP = $(OCAMLFIND) ocamldep -package "$(REQUIRES)"
 LINK_OPTIONS = -thread -package threads -linkpkg
 TUTORS_TEMPLATE = hbugs_tutor.TPL.ml
 TUTORS_INDEX = INDEX.xml
@@ -52,4 +53,5 @@ clean:
 distclean: clean
 	rm -f run/*
 .PHONY: all world byte opt clean start stop
+.PRECIOUS: %.cmi