diff options
| author | filliatr | 2001-09-19 14:15:09 +0000 |
|---|---|---|
| committer | filliatr | 2001-09-19 14:15:09 +0000 |
| commit | cd5694905bd7e4f852aa0dbc62a2de1abd0366f8 (patch) | |
| tree | dc270626a2191a6003f5191b2ccf4bfed78e5962 /tools | |
| parent | 242f8d2e8afb7da4302c07c2f1f8148bfa362b85 (diff) | |
make install dans coq_makefile et repertoire associe user-contrib ajoute au load path au demarrage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1999 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d22072cd35..fcfd00cb40 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -97,9 +97,9 @@ let standard sds = sds; print "\n"; print "install:\n"; - print "\t@if test -z $(TARGETDIR); then echo \"You must set TARGETDIR (for instance with 'make TARGETDIR=foobla install')\"; exit 1; fi\n"; - if !some_vfile then print "\tcp -f *.vo $(TARGETDIR)\n"; - if !some_mlfile then print "\tcp -f *.cmo $(TARGETDIR)\n"; + print "\tmkdir -p `$(COQC) -where`/user-contrib\n"; + if !some_vfile then print "\tcp -f *.vo `$(COQC) -where`/user-contrib\n"; + if !some_mlfile then print "\tcp -f *.cmo `$(COQC) -where`/user-contrib\n"; List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n") sds; |
