svn commit: r426358 - head/math/coq
Alexey Dokuchaev
danfe at FreeBSD.org
Sat Nov 19 11:39:41 UTC 2016
Author: danfe
Date: Sat Nov 19 11:39:40 2016
New Revision: 426358
URL: https://svnweb.freebsd.org/changeset/ports/426358
Log:
- Move license information from port description into LICENSE knobs
- Convert $arch-conditional BROKEN statement into BROKEN_$arch one
Modified:
head/math/coq/Makefile
head/math/coq/pkg-descr
Modified: head/math/coq/Makefile
==============================================================================
--- head/math/coq/Makefile Sat Nov 19 11:33:05 2016 (r426357)
+++ head/math/coq/Makefile Sat Nov 19 11:39:40 2016 (r426358)
@@ -12,6 +12,9 @@ DISTNAME= ${PORTNAME}-${COQVERSION}
MAINTAINER= johans at FreeBSD.org
COMMENT= Theorem prover based on lambda-C
+LICENSE= LGPL21
+LICENSE_FILE= ${WRKSRC}/LICENSE
+
BUILD_DEPENDS= camlp5:devel/ocaml-camlp5 \
ocamlfind:devel/ocaml-findlib
@@ -27,12 +30,14 @@ CONFIGURE_ARGS= --prefix ${PREFIX} \
--opt
MAKE_ENV= COQINSTALLPREFIX=${DESTDIR}
+BROKEN_powerpc= does not link
+
OPTIONS_DEFINE= DOCS IDE
OPTIONS_DEFAULT= IDE
OPTIONS_SUB= yes
IDE_DESC= Include desktop environment (coqide)
IDE_BUILD_DEPENDS= lablgtk2:x11-toolkits/ocaml-lablgtk2
-IDE_RUN_DEPENDS:= lablgtk2:x11-toolkits/ocaml-lablgtk2
+IDE_RUN_DEPENDS= lablgtk2:x11-toolkits/ocaml-lablgtk2
IDE_CONFIGURE_OFF= --coqide no
DOCS_USE= TEX=latex:build,dvipsk:build,texmf:build
DOCS_BUILD_DEPENDS= hevea:textproc/hevea
@@ -43,12 +48,6 @@ PORTDOCS= *
add-plist-post:
@${DO_NADA}
-.include <bsd.port.pre.mk>
-
-.if ${ARCH} == "powerpc"
-BROKEN= Does not link on powerpc
-.endif
-
post-patch:
@${REINPLACE_CMD} -e '/FreeBSD.*\.byte/s/^/#/' \
-e '1s:/bin/bash:/bin/sh:' \
@@ -57,6 +56,7 @@ post-patch:
${WRKSRC}/Makefile* ${WRKSRC}/install.sh
@${REINPLACE_CMD} -e '/^#COQINSTALLPREFIX/{s/^#//;s|$$|$${DESTDIR}|;}' \
${WRKSRC}/Makefile.build
- @${REINPLACE_CMD} -e '/show_latex_mes/s/)$$/; true)/' ${WRKSRC}/Makefile.doc
+ @${REINPLACE_CMD} -e '/show_latex_mes/s/)$$/; true)/' \
+ ${WRKSRC}/Makefile.doc
-.include <bsd.port.post.mk>
+.include <bsd.port.mk>
Modified: head/math/coq/pkg-descr
==============================================================================
--- head/math/coq/pkg-descr Sat Nov 19 11:33:05 2016 (r426357)
+++ head/math/coq/pkg-descr Sat Nov 19 11:39:40 2016 (r426358)
@@ -1,5 +1,3 @@
-From the website:
-
Developed in the LogiCal project, the Coq tool is a formal proof
management system: a proof done with Coq is mechanically checked
by the machine.
@@ -14,9 +12,6 @@ Coq is based on a logical framework call
Constructions" extended by a modular development system for
theories.
-Coq is distributed under the GNU Lesser General Public Licence
-Version 2.1 (LGPL).
-
CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.
-WWW: http://coq.inria.fr/
+WWW: http://coq.inria.fr/
More information about the svn-ports-all
mailing list