aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-07-02 06:51:13 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-07-02 06:51:13 +0000
commit303a60fb220af34b854115e4787962185e119816 (patch)
tree6ba4d76c035d9d3b8200034a655fdcd274818b88 /tools
parent7c290a484d4167d91fbe2de84bba6931e2e2dd8f (diff)
rm -f .depend (sans le -f "make depend" echoue lorsque le .depend
n'existe pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 9267145df..a71315ca8 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -86,7 +86,7 @@ let standard sds =
if !some_file then print "include .depend\n\n";
print ".depend depend:\n";
if !some_file then begin
- print "\trm .depend\n";
+ print "\trm -f .depend\n";
print "\t$(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend\n";
print "\t$(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend\n";
end;