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>