diff options
| author | letouzey | 2008-05-22 11:21:47 +0000 |
|---|---|---|
| committer | letouzey | 2008-05-22 11:21:47 +0000 |
| commit | c941fc98f9a707b2a81eb3a1b36d1f497632b04b (patch) | |
| tree | a1424a564568e84d1752828281ce0b10d7be17ff /dev | |
| parent | cf73432c0e850242c7918cc348388e5cde379a8f (diff) | |
Should fix the dependancy issue mentioned by J.Forest about NMake:
.v.d are created exactly for all $(VFILES), which was only a
"find -name .v", so $(GENVFILES) should be added to $(VFILES)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10965 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions