diff options
author | Matthieu Sozeau <mattam@gentoo.org> | 2006-02-04 17:15:51 +0000 |
---|---|---|
committer | Matthieu Sozeau <mattam@gentoo.org> | 2006-02-04 17:15:51 +0000 |
commit | 2b7e78164d3f1cd63223bcf714566b4963426acc (patch) | |
tree | 75f58cfbd08d80af99803048dec14dd7c2866e7f | |
parent | Mark 2.12.0 stable on alpha (diff) | |
download | gentoo-2-2b7e78164d3f1cd63223bcf714566b4963426acc.tar.gz gentoo-2-2b7e78164d3f1cd63223bcf714566b4963426acc.tar.bz2 gentoo-2-2b7e78164d3f1cd63223bcf714566b4963426acc.zip |
Remove old version, incompatible with current ocaml and move current to stable (over a year of testing:)
(Portage version: 2.0.51.22-r1)
-rw-r--r-- | sci-mathematics/coq/ChangeLog | 6 | ||||
-rw-r--r-- | sci-mathematics/coq/coq-7.4.ebuild | 40 | ||||
-rw-r--r-- | sci-mathematics/coq/coq-8.0-r1.ebuild | 4 | ||||
-rw-r--r-- | sci-mathematics/coq/files/digest-coq-7.4 | 1 |
4 files changed, 7 insertions, 44 deletions
diff --git a/sci-mathematics/coq/ChangeLog b/sci-mathematics/coq/ChangeLog index 4365618b17e1..9ac848b86bfe 100644 --- a/sci-mathematics/coq/ChangeLog +++ b/sci-mathematics/coq/ChangeLog @@ -1,6 +1,10 @@ # ChangeLog for sci-mathematics/coq # Copyright 2000-2006 Gentoo Foundation; Distributed under the GPL v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.4 2006/02/04 16:30:27 mattam Exp $ +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/ChangeLog,v 1.5 2006/02/04 17:15:51 mattam Exp $ + + 04 Feb 2006; Matthieu Sozeau <mattam@gentoo.org> -coq-7.4.ebuild, + coq-8.0-r1.ebuild: + Remove old 7.4 version and move 8.0-r1 to stable on x86 and ppc. *coq-8.0_p3 (04 Feb 2006) diff --git a/sci-mathematics/coq/coq-7.4.ebuild b/sci-mathematics/coq/coq-7.4.ebuild deleted file mode 100644 index 34d6b1b16bab..000000000000 --- a/sci-mathematics/coq/coq-7.4.ebuild +++ /dev/null @@ -1,40 +0,0 @@ -# Copyright 1999-2006 Gentoo Foundation -# Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-7.4.ebuild,v 1.3 2006/02/04 16:30:27 mattam Exp $ - -inherit eutils - -DESCRIPTION="Coq is a proof assistant written in O'Caml" -HOMEPAGE="http://coq.inria.fr/" -SRC_URI="ftp://ftp.inria.fr/INRIA/${PN}/V${PV}/${P}.tar.gz" - -LICENSE="LGPL-2.1" -SLOT="0" -KEYWORDS="x86 ppc ~amd64" -IUSE="norealanalysis" - -DEPEND=">=dev-lang/ocaml-3.06 -!>=dev-lang/ocaml-3.08" - -src_compile() { - local myconf="--prefix /usr \ - --bindir /usr/bin \ - --libdir /usr/lib/coq \ - --mandir /usr/man \ - --emacslib /usr/share/emacs/site-lisp" - - use norealanalysis \ - && myconf="$myconf --reals" \ - || myconf="$myconf --reals all" - - has_version ">=dev-lang/ocaml-3.07" && epatch ${FILESDIR}/ocaml-3.07.patch - - ./configure $myconf || die - - emake world || die -} - -src_install() { - make COQINSTALLPREFIX=${D} install || die - dodoc README CREDITS CHANGES -} diff --git a/sci-mathematics/coq/coq-8.0-r1.ebuild b/sci-mathematics/coq/coq-8.0-r1.ebuild index 24f89697c548..68b030deb7b6 100644 --- a/sci-mathematics/coq/coq-8.0-r1.ebuild +++ b/sci-mathematics/coq/coq-8.0-r1.ebuild @@ -1,6 +1,6 @@ # Copyright 1999-2006 Gentoo Foundation # Distributed under the terms of the GNU General Public License v2 -# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0-r1.ebuild,v 1.3 2006/02/04 16:30:27 mattam Exp $ +# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/coq/coq-8.0-r1.ebuild,v 1.4 2006/02/04 17:15:51 mattam Exp $ inherit eutils @@ -18,7 +18,7 @@ translator? ( ftp://ftp.inria.fr/INRIA/coq/V${MY_PV}/${MY_P}-translator.tar.gz ) LICENSE="LGPL-2.1" SLOT="0" -KEYWORDS="~x86 ~ppc ~sparc ~amd64" +KEYWORDS="x86 ppc ~sparc ~amd64" DEPEND=">=dev-lang/ocaml-3.06 ide? ( >=dev-ml/lablgtk-2.2.0 )" diff --git a/sci-mathematics/coq/files/digest-coq-7.4 b/sci-mathematics/coq/files/digest-coq-7.4 deleted file mode 100644 index ab1d3353a4d9..000000000000 --- a/sci-mathematics/coq/files/digest-coq-7.4 +++ /dev/null @@ -1 +0,0 @@ -MD5 13ac61f150823e54ad84a9096e2dd646 coq-7.4.tar.gz 1537547 |