diff options
| author | filliatr | 2001-04-19 15:07:41 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-19 15:07:41 +0000 |
| commit | 8a009c8729dd6905dd7d47877b444fa38dd2e221 (patch) | |
| tree | 70f689960f99506af4f3d56796ea972e47193f21 /contrib/extraction/test/Makefile | |
| parent | fe45801c1fdfebeacaf5daa0569d89838b11774f (diff) | |
blindage False_rec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/Makefile')
| -rw-r--r-- | contrib/extraction/test/Makefile | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 2a29f866ac..994d7cf2c7 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -31,7 +31,8 @@ allcmo: .names.cmo $(CMONAMES) .names.ml: Makefile v2ml rm -f .names.ml; \ echo "MLNAMES= \\" > .names.ml; \ - find theories -name \*.v -exec ./v2ml \{\} \; | \ + V2ML=`pwd`/v2ml; \ + (cd $(TOPDIR); find theories -name \*.v -exec $$V2ML \{\} \;) | \ sed -e "s/\.ml/.ml \\\\/" >> .names.ml .names.cmo: .names.ml @@ -39,9 +40,8 @@ allcmo: .names.cmo $(CMONAMES) sed -e "1s/ML/CMO/" -e "s/\.ml/.cmo/" < .names.ml > .names.cmo tree: - for f in `cd $(TOPDIR); find theories -name \*.v`; do \ - mkdir -p `dirname $$f`; \ - cp $(TOPDIR)/$$f $$f; \ + for f in `cd $(TOPDIR); find theories -type d ! -name CVS`; do \ + mkdir -p $$f; \ done ml2v: ml2v.ml |