Skip site navigation (1)Skip section navigation (2)
Date:      Sat, 19 Nov 2016 11:39:40 +0000 (UTC)
From:      Alexey Dokuchaev <danfe@FreeBSD.org>
To:        ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org
Subject:   svn commit: r426358 - head/math/coq
Message-ID:  <201611191139.uAJBdeve028322@repo.freebsd.org>

next in thread | raw e-mail | index | archive | help
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@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/



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201611191139.uAJBdeve028322>